Intersection Types from a Proof-theoretic Perspective

• Autorzy: Pimentel E. , Ronchi della Rocca S. , Roversi L.
• Języki publikacji: EN

Abstrakty

EN

In this work we present a proof-theoretical justification for the intersection type assignment system (IT) by means of the logical system Intersection Synchronous Logic (ISL). ISL builds classes of equivalent deductions of the implicative and conjunctive fragment of the intuitionistic logic (NJ). ISL results from decomposing intuitionistic conjunction into two connectives: a synchronous conjunction, that can be used only among equivalent deductions of NJ, and an asynchronous one, that can be applied among any sets of deductions of NJ. A term decoration of ISL exists so that it matches both: the IT assignment system, when only the synchronous conjunction is used, and the simple types assignment with pairs and projections, when the asynchronous conjunction is used. Moreover, the proof of strong normalization property for ISL is a simple consequence of the same property in NJ and hence strong normalization for IT comes for free.

Słowa kluczowe

EN

intersection types; lambda calculus; type assignment systems; structural proof-theory

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 121, nr 1/4
• Strony: 253--274
• Opis fizyczny: Bibliogr. 22 poz.

Twórcy

autor

Pimentel E.

autor

Ronchi della Rocca S.

autor

Roversi L.

• Departamento de Matematicas, Universidad del Valle, Colombia and Departamento de Matematica, Universidade Federal de Minas Gerais, Brazil,

Bibliografia

• [1] Alessi, F. and Barbanera, F.; Strong conjunction and intersection types. In 16th International Symposium on Mathematical Foundation of Computer Science (MFCS91), volume Lecture Notes in Computer Science 520. Springer-Verlag, 1991.
• [2] Avron, A.; Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artficial Intelligence 4, 225-248, 1991.
• [3] Barbanera, F. and Martini, S.; Proof-functional connectives and realizability. Archive for Mathematical Logic, 33:189-211, 1994.
• [4] Capitani, B., Loreti, M., and Venneri B.; Hyperformulae, parallel deductions and intersection types. Electronic Notes in Theoretical Computer Science, 50(2), 2001.
• [5] Coppo, M. and Dezani-Ciancaglini, M.; An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4):685-693, 1980.
• [6] Curry H.B. and R. Feys.; Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958.
• [7] Dezani-Ciancaglini, M., Ghilezan, S., and Venneri, B.; The "relevance" of intersection and union types. Notre Dame J. Formal Logic, 38(2):246-269, 1997.
• [8] Girard, J-Y.; The System F of Variable Types: Fifteen Years Later. Theoretical Computer Science, vol. 45, pp.159-192, 1986.
• [9] Girard, J-Y.; Linear Logic. Theoretical Computer Science, 50:1-102, 1987.
• [10] Girard, J-Y., Lafont, Y., and Taylor, P.; Proofs and types. Cambridge University Press, 1989.
• [11] Hindley, J.R.; Coppo Dezani types do not correspond to propositional logic. Theoret. Comput. Sci., 28(1-2):235-236, 1984.
• [12] Liquori, L. and Ronchi Della Rocca, S.; Intersection Types `a la Church. Information and Computation, 205(9):1371-1386, 2007.
• [13] Lopez-Escobar, E. K. G.; Proof-functional connectives. Methods of Mathematical Logic, Proceedings of the 6th Latin-American Symposium on Mathematical Logic, Caracas, 1983 LNCS, 1130:208-221, 1985.
• [14] Pottinger, G.; A type assignment for the strongly normalizable _-terms. In To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, pages 561-577. Academic Press, London, 1980.
• [15] Reynolds, J. C.; Towards a type theory of type structure. Programming Symposium, LNCS 19, pp. 408-425, 1974.
• [16] Reynolds, J. C.; Design of the programming language Forsythe. In P. O'Hearn and R. D. Tennent editors, Algol-like Languages, Birkhauser, 1996.
• [17] Ronchi Della Rocca, S.; Typed Intersection Lambda Calculus. In LTRS 2002, volume 70(1) of Electronic Notes in Computer Science. Elsevier, 2002.
• [18] Ronchi della Rocca, S., Roversi, L.; Intersection Logic. In Proceedings of CSL'01, volume 2142 of LNCS, pages 414-428. Springer-Verlag, 2001.
• [19] Stavrinos, Y., Veneti, A.; Of kits and molecules. In Proceedings. of the 6th Panellenic Logic Symposium, Kaury, G. and Zachos, S. (eds), pages 125-131, 2007.
• [20] Tait, W.W.; Intensional interpretation of functions of finite type I. Journal of Symbolic Logic, 32:198-212, 1967.
• [21] Venneri, B.; Intersection types as logical formulae. J. Logic Comput., 4(2):109-124, 1994.
• [22] Wells, J. B. and Haack, C.; Branching types. In Programming Languages & Systems, 11th European Symp. Programming, volume 2305 of LNCS, pages 115-132. Springer-Verlag, 2002.