Towards a Logic for Union Types

• Autorzy: Stavrinos Y. , Veneti A.
• Języki publikacji: EN

Abstrakty

EN

We examine a logical foundation for the intersection and union types assignment system (IUT). The proposed system is Intersection and Union Logic (IUL), an extension of Intersection Logic (IL) with the canonical rules for union. We investigate two different formalisms for IUL, as well as its properties and its relation with minimal intuitionistic logic.

Słowa kluczowe

EN

intersection types; union types; intersection logics; kits; molecules

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

Twórcy

autor

Stavrinos Y.

autor

Veneti A.

• Graduate Program in Logic, Algorithms, and Computation Department of Mathematics University of Athens GR-15784 Zografou, Greece,

Bibliografia

• [1] Barbanera F., Dezani-Ciancaglini M., and de'Liguoro U., Intersection and Union Types: Syntax and Semantics, Information and Computation 119, pp. 202-230, Academic Press, 1995.
• [2] Bono V., Venneri B., and Bettini L., A Typed Lambda Calculus with Intersection Types, Theoretical Computer Science 398, pp. 95-113, Elsevier, 2008.
• [3] Capitani B., Loreti M., and Venneri B., Hyperformulae, Parallel Deductions, and Intersection Types, Proceedings of ICALP'01 Workshop: BOTH 2001, Electronic Notes in Theoretical Computer Science 50(2), pp. 178-195, 2001.
• [4] Dezani-Ciancaglini M., Ghilezan S., and Venneri B., The "Relevance" of Intersection and Union Types, Notre Dame Journal of Formal Logic 38(2), pp. 246-269, 1997.
• [5] Liquori L. and Ronchi della Rocca S., Intersection-Types `a la Church, Information and Computation 205(9), pp. 1371-1386, Elsevier, 2007.
• [6] Pimentel E., Ronchi della Rocca S., and Roversi L., Intersection Types: a Proof-Theoretical Approach, ICALP'05 Workshop, Proceedings of Structures and Deduction, pp. 189-204, 2005.
• [7] Pimentel E., Ronchi della Rocca S., and Roversi L., Intersection Types from a prooftheoretic perspective, 4th Workshop on Intersection Types and Related Systems, Torino, 2008. (http://imft.ftn.ns.ac.yu/ITRS08/itrs08 5 epsrdrlr.pdf)
• [8] Ronchi della Rocca S., Intersection Typed λ-calculus, Proceedings of 2nd Workshop on Intersection Types and Related Systems, Electronic Notes in Theoretical Computer Science 70(1), pp. 163-181, Elsevier Science, 2002.
• [9] Ronchi della Rocca S. and Roversi L., Intersection Logic, Proceedings of CSL'01, Lecture Notes in Computer Science 2142, pp. 414-428, Springer-Verlag, 2001.
• [10] Stavrinos Y. and Veneti A., Of kits and molecules, Proceedings of 6th Panhellenic Logic Symposium, pp. 125-131, University of Thessaly, 2007. (http://www.math.ntua.gr/_gstav/kmpls07.pdf)
• [11] Veneti A., On a Logical Foundation of the Intersection Types Assignment System: Intersection Logics, Master's Thesis, Graduate Program in Logic, Algorithms, and Computation (MPLA), University of Athens, 2007. (http://mpla.math.uoa.gr/msc/ files/A.Veneti.pdf)
• [12] Veneti A. and Stavrinos Y., Towards an intersection and union logic, 4th Workshop on Intersection Types and Related Systems, Torino, 2008. (http://imft.ftn.ns.ac.yu/ITRS08/itrs08 6 avys.pdf)
• [13] Veneti A. and Stavrinos Y., A Sequent Calculus for Intersection and Union Logic, Local Proceedings of 4th Conference on Computability in Europe, p. 514(524), University of Athens, 2008. (http://www.cs.swan.ac.uk/cie08/cie2008-local.pdf)
• [14] Wells J.B., Dimock A., Muller R., and Turbak F., A Calculus with Polymorphic and Polyvariant Flow Types, Journal of Functional Programming 12(3), pp. 183-227, Cambridge University Press, 2002.
• [15] Wells J.B. and Haack C., Branching Types, Proceedings of 11th European Symposium on Programming, Lecture Notes in Computer Science 2305, pp. 115-132, Springer-Verlag, 2002