Abstract | ||
---|---|---|
We present a general method for constructing extensional models for the polymorphic lambda calculus—the polymorphic extensional collapse. The method yields models that satisfy additional, computationally motivated constraints like having only two polymorphic booleans and having only the numerals as polymorphic integers. Moreover the method yields models that prove that the polymorphic lambda calculus can be conservatively added to arbitrary algebraic data type specifications, even with complete transfer of the computational power to the added data types. |
Year | DOI | Venue |
---|---|---|
1987 | 10.1016/0304-3975(88)90097-7 | II and Colloquium on Functional and Logic Programming and Specifications (CFLP) on TAPSOFT '87: Advanced Seminar on Foundations of Innovative Software Development |
Keywords | DocType | Volume |
extensional models,extensional model,polymorphism,satisfiability,data type,lambda calculus | Conference | 59 |
Issue | ISSN | ISBN |
1-2 | Theoretical Computer Science | 3-540-17611-X |
Citations | PageRank | References |
18 | 2.70 | 12 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
V. Breazu-Tannen | 1 | 23 | 4.49 |
T. Coquand | 2 | 135 | 13.55 |