Abstract
The meaning of a formula built out of proof-functional connectives depends in an essential way upon the intensional aspect of the proofs of the component subformulas. We study three such connectives, strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), strong conjunction (where the two components of the conjunction are established by the same proof) and relevant implication (where the implication is established by an identity map). For each of these connectives we give a type assignment system, a realizability semantics, and a completeness theorem. This form of completeness implies the semantic completeness of the type assignment system.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
[Anderson & Belnap 75] Anderson A., Belnap N.: Entailment vol. I, Princeton, Princeton University Press 1975
[Alessi & Barbanera 91] Alessi F., Barbanera F.: Strong conjunction and intersection types, Lect. Notes Comput. Sci.520, 64–73 (1991)
[Barendegt 1984] Barendregt H.: The lambda calculus: its syntax and semantics, Amsterdam: North Holland (1984)
[Barendregt et al. 83] Barendregt H., Coppo M., Dezani M.: A filter lambda model and the completeness of type assignment. J. Symb. Logic48(4), 931–940 (1983)
[Bruce & Longo 85] Bruce K., Longo G.: Provable isomorphisms and domain equations in models of typed languages. ACM Symp. Theory Computing (1985)
[Bruce et al. 92] Bruce K., Di Cosmo R., Longo G.: Provable isomorphisms of types. Math. Struct. Comp. Sci.2(2), 231–247 (1992)
[Coppo & Dezani 80] Coppo M., Dezani M.: An extension of basic functionality theory for lambdacalculus. Notre Dame Journal of Formal Logic21(4), 685–693 (1980)
[Coppo et al. 82] Coppo M., Dezani M., Honsell F., Longo G.: Extended type structures and filter lambda models. Proc. Logic Colloquium '82, Lolli G., Longo G., Marcja A. (eds), pp 241–262, North-Holland (1984)
[Curry & Feys 58] Curry H.B., Feys R.: Combinatory Logic vol. I. Amsterdam: North Holland 1958
[Dezani & Hindley 89] Dezani M., Hindley R.: Intersection types for combinatory logic. Theoretical Computer Science100, 303–324 (1992)
[Di Cosmo 91] Di Cosmo R.: Provable isomorphisms of second order types. Rapport de Recherche du Laboratoire d'Informatique de l'Ecole Normal Supérieure, Paris (1991)
[Kleene 52] Kleene S.C.: Permutability of inferences in Gentzen's calculi LK and LJ. MAMS10, 1–26 (1952)
[Lopez-Escobar 85] Lopez-Escobar E.G.K.: Proof functional connectives. Lect. Notes Math.1130, 208–221 (1985).
[Martini 92] S. Martini: Provable isomorphisms, strong equivalence, and realizability. Proceedings IV Conferenza Italiana di Informatica Teorica, Venturini-Zilli M., Marchetti-Spaccamela A. (eds.), pp 258–268. World Scientific Pub. 1992
[Meyer 82] Meyer A.: What is a model of the lambda calculus?, Inf. Comput.52, 87–122 (1982)
[Meyer & Routley 72a] Meyer R.K., Routley R.: Algebraic analysis of entailment I. Logique et Analyse15, 407–428 (1972)
[Meyer & Routley 72b] Meyer R.K., Routley R.: Semantics of entailment III. J. Philos. Logic1, 192–208 (1972)
[Mints 89] Mints G.E.: The completeness of provable realizability. Notre Dame J. Formal Logic30(3), 420–441 (1989)
[Mints 91] Mints G.E.: Personal communication (1991)
[Pottinger 80] Pottinger G.: A type assignment for the strongly normalizable λ-terms. In: Hindley R., Seldin J. (eds.) to H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism. Academic Press (1980), pp. 561–577
[Rittri 90] Rittri M.: Using types as search keys in function libraries. J. Funct. Program.1(1), 71–90 (1990)
[Takeuti 75] Takeuti G.: Proof Theory. Amsterdam: North-Holland Publishing Company 1975
[Venneri 92] Venneri B.: Intersection types as logical formulas. Internal report Dipartimento di Informatica Università di Torino, submitted for publication 1992