Provable isomorphisms of types - ENS - École normale supérieure Accéder directement au contenu
Article Dans Une Revue Mathematical Structures in Computer Science Année : 1992

Provable isomorphisms of types


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.
Fichier principal
Vignette du fichier
2021_08_10_Provable_isomorphisms_of_types.pdf (240.02 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03316287 , version 1 (10-08-2021)



Kim Bruce, Roberto Di Cosmo, Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 1992, 2 (2), pp.231-247. ⟨10.1017/S0960129500001444⟩. ⟨hal-03316287⟩
33 Consultations
36 Téléchargements



Gmail Facebook Twitter LinkedIn More