Accéder directement au contenu Accéder directement à la navigation
Article dans une revue

Provable isomorphisms of types

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.
Type de document :
Article dans une revue
Liste complète des métadonnées

https://hal-ens.archives-ouvertes.fr/hal-03316287
Contributeur : Usr 3608 République Des Savoirs <>
Soumis le : mardi 10 août 2021 - 15:55:59
Dernière modification le : mercredi 11 août 2021 - 03:19:17

Fichier

2021_08_10_Provable_isomorphis...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Kim Bruce, Roberto Di Cosmo, Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 1992, 2 (2), pp.231-247. ⟨10.1017/S0960129500001444⟩. ⟨hal-03316287⟩

Partager

Métriques

Consultations de la notice

27

Téléchargements de fichiers

5