Intersection Types with Subtyping by Means of Cut Elimination

• Autorzy: Laurent O.
• Języki publikacji: EN

Abstrakty

EN

We give a purely syntactic proof (from scratch) of the subject equality property of the BCD intersection type system through a reformulation of the subtyping relation having a "cut- elimination" property.

Słowa kluczowe

EN

intersection types; cut elimination

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

Twórcy

autor

Laurent O.

• Laboratoire de l’Informatique du Parallelisme Universite de Lyon, ENS Lyon, CNRS, UCBL, INRIA, France,

Bibliografia

• [1] van Bakel, S.: Intersection Type Assignment Systems, Theoretical Computer Science, 151(2), 1995, 385-435.
• [2] Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A Filter Lambda Model and the Completeness of Type Assignment, Journal of Symbolic Logic, 48, 1983, 931-940.
• [3] Coppo, M., Dezani-Ciancaglini, M., Honsell, F., Longo, G.: Extended Type Structures and Filter Lambda Models, Logic Colloquium 82 (G. Lolli, G. Longo, A. Marcja, Eds.), 112, North-Holland, 1984.
• [4] Coppo, M., Dezani-Ciancaglini, M., Zacchi, M.: Type Theories, Normal Forms and D1-Lambda-Models, Information and Computation, 72(2), 1987, 85-116.
• [5] Dezani-Ciancaglini, M., Ghilezan, S., Venneri, B.: The "Relevance" of Intersection and Union Types, Notre Dame Journal of Formal Logic, 38(2), 1997, 246-269.
• [6] Ishihara, H., Kurata, T.: Completeness of intersection and union type assignment systems for call-by-value lambda-models, Theoretical Computer Science, 272(1-2), 2002, 197-221.
• [7] Marion, J.-Y.: From multiple sequent for Additive Linear Logic to decision procedures for Free Lattices, Theoretical Computer Science, 224(1-2), 1999, 157-172.
• [8] Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda Calculus, Texts in Theoretical Computer Science, Springer, 2004.
• [9] Whitman, P.: Free lattices, Annals of Mathematics, 42(1), January 1941, 325-330.