Provable isomorphisms of types

Mathematical Structures in Computer Science - Tập 2 Số 2 - Trang 231-247 - 1992
Kim B. Bruce1, Roberto Di Cosmo2, G. Longo3
1Williams College [Williamstown] (Williams College, 18 Hoxsey Street, Williamstown, MA 01267, USA - États-Unis)
2DI - Dipartimento di Informatica [Pisa] (University of Pisa Dipartimento di Informatica Largo B. Pontecorvo, 3 (formerly via F. Buonarroti, 2) I-56127 Pisa - Italie)
3LIENS - Laboratoire d'informatique de l'école normale supérieure (45 Rue d'Ulm 75230 PARIS CEDEX 05 - France)

Tóm tắt

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.

Từ khóa


Tài liệu tham khảo

10.1007/BF02023009

10.1007/BF01084396

10.1007/3-540-52885-7_117

Rittri, 1989, Using types as search keys in function libraries, Journal of Functional Programming, 1

Reynolds J.C. (1984) Polymorphism is not set-theoretic. Lecture Notes in Computer Science, 173.

Martini, 1991, Strong equivalence in positive propositional logic: provable realizability and type assignment

Martin, 1972, Axiomatic bases for equational theories of natural numbers, Notices of the Am. Math. Soc., 19, 778

Lambek, 1986, An introduction to higher order categorical logic

10.1007/BFb0075313

Curien, 1991, ICALP, 291

Barendregt, 1984, The Lambda Calculus; Its syntax and Semantics (revised edition)

Narendran P. , Pfenning F. and Statman R. (1989) On the unification problem for cartesian closed categories. Hardware Verification Workshop, 09 1989.

10.1016/0304-3975(76)90085-2

Bruce K. and Longo G. (1985) Provable isomorphisms and domain equations in models of typed languages. ACM Symposium on Theory of Computing (STOC 85).

Asperti, 1991, Categories, Types, and Structures

10.1305/ndjfl/1093883461

Di Cosmo R. and Longo G. (1989) Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). Workshop on Logic for Computer Science – MSRI, Berkeley.

Babaev A. A. and Soloviev S. V. (1982) Coherence theorem for canonical maps in certesian closed categories. Journal of Soviet Mathematics, 20.

Alessi F. and Barbanera F. (1991) Strong conjunction and intersection types. Dipartimento di Informatica, Università di Torino (Italy), manuscript.

Thông tin
Thông tin xuất bản

Mathematical Structures in Computer Science

Tập 2 Số 2

231-247

Thông tin tác giả