Name
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 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 of this design. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1145/1086365.1086375 | Proceedings of the tenth ACM SIGPLAN international conference on Functional programming |
Keywords | Field | DocType |
type system,dependent types,ats,programming paradigm,theorem proving | Constraint satisfaction,Programming language,Programming paradigm,Computer science,Automated theorem proving,Inductive programming,Constraint programming,Proof theory,Type theory,Theoretical computer science,Reactive programming | Conference |
Volume | Issue | ISSN |
40 | 9 | 0362-1340 |
ISBN | Citations | PageRank |
1-59593-064-7 | 56 | 2.44 |
References | Authors | |
13 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chiyan Chen | 1 | 95 | 5.37 |
| Hongwei Xi | 2 | 652 | 56.11 |