Provable isomorphisms of types
- 1 June 1992
- journal article
- research article
- Published by Cambridge University Press (CUP) in Mathematical Structures in Computer Science
- Vol. 2 (2) , 231-247
- https://doi.org/10.1017/s0960129500001444
Abstract
A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. Using the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC's. Using the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having “invertible” proofs between the two terms. Work of Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.Keywords
This publication has 10 references indexed in Scilit:
- Strong conjunction and intersection typesPublished by Springer Nature ,1991
- Using types as search keys in function librariesJournal of Functional Programming, 1991
- Retrieving library identifiers via equational matching of typesPublished by Springer Nature ,1990
- Provable isomorphisms and domain equations in models of typed languagesPublished by Association for Computing Machinery (ACM) ,1985
- Proof functional connectivesLecture Notes in Mathematics, 1985
- Polymorphism is not set-theoreticPublished by Springer Nature ,1984
- λ-definable functionals andβη conversionArchive for Mathematical Logic, 1983
- The category of finite sets and Cartesian closed categoriesJournal of Mathematical Sciences, 1983
- The Church-Rosser theorem for the typed $\lambda$-calculus with surjective pairing.Notre Dame Journal of Formal Logic, 1981
- Characterization of normal forms possessing inverse in the λ-β-η-calculusTheoretical Computer Science, 1976