Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
inproceedings{CPwTP-icfp05, author = "Chiyan Chen and Hongwei Xi", title = {{Combining Programming with Theorem Proving}}, booktitle = "Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming", year = 2005, month = "September", address = "Tallinn, Estonia", pages = "66--77", abstract = {{ Applied Type System (ATS) is recently proposed as a framework for designing and formalizing (advanced) type systems in support of practical programming. In ATS, the definition of type equality involves a constraint relation, which may or may not be algorithmically decidable. To support practical programming, we adopted a design in the past that imposes certain restrictions on the syntactic form of constraints so that some effective means can be found for solving constraints automatically. Evidently, this is a rather {\em ad hoc} design in its nature. In this paper, we rectify the situation by presenting a fundamentally different design, which we claim to be both novel and practical. Instead of imposing syntactical restrictions on constraints, we provide a means for the programmer to construct proofs that attest to the validity of constraints. In particular, we are to accommodate a programming paradigm that enables the programmer to combine programming with theorem proving. Also we present some concrete examples in support of the practicality this design. }} }