Completeness and Soundness Results for χ with Intersection and Union Types

• Autorzy: Bakel S. van
• Języki publikacji: EN

Abstrakty

EN

With the eye on defining a type-based semantics, this paper defines intersection and union type assignment for the sequent calculus χ, a substitution-free language that enjoys the Curry- Howard correspondence with respect to the implicative fragment of Gentzen's sequent calculus for classical logic. We investigate the minimal requirements for such a system to be complete (i.e. closed under redex expansion), and show that the non-logical nature of both intersection and union types disturbs the soundness (i.e. closed uder reduction) properties. This implies that this notion of intersection-union type assignment needs to be restricted to satisfy soundness as well, making it unsuitable to define a semantics. We will look at two (confluent) notions of reduction, called Call-by-Name and Call-by- Value, and prove soundness results for those.

Słowa kluczowe

EN

classical logic; sequent calculus; intersection types; union types

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

Twórcy

autor

Bakel S. van

• Department of Computing, Imperial College London, UK 180 Queen's Gate, London SW7 2BZ, UK,

Bibliografia

• [1] Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus, Proceedings of the Fourth ACM Conference on Computer and Communications Security, ACM Press, 1997.
• [2] Bakel, S. van: Complete restrictions of the Intersection Type Discipline, Theoretical Computer Science, 102(1), 1992, 135-163.
• [3] Bakel, S. van: Intersection Type Assignment Systems, Theoretical Computer Science, 151(2), 1995, 385-435.
• [4] Bakel, S. van: Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalising, Notre Dame journal of Formal Logic, 45(1), 2004, 35-63.
• [5] Bakel, S. van: Intersection and Union Types for X, Electronic Proceedings of 3rd International Workshop Intersection Types and Related Systems (ITRS'04), Turku, Finland, 136, 2004.
• [6] Bakel, S. van: Reduction in X does not agree with Intersection and Union Types, Electronic Proceedings of 4th International Workshop Intersection Types and Related Systems (ITRS'08), Turin, Italy, 2008.
• [7] Bakel, S. van: Completeness and Partial Soundness Results for Intersection & Union Typing for λμ˜μ, Annals of Pure and Applied Logic, 161, 2010, 1400-1430.
• [8] Bakel, S. van, Cardelli, L., Vigliotti, M.: From X to π; Representing the Classical Sequent Calculus in the π-calculus, Electronic Proceedings of International Workshop on Classical Logic and Computation 2008 (CL&C'08), Reykjavik, Iceland, 2008.
• [9] Bakel, S. van, de'Liguoro, U.: Logical equivalence for subtyping object and recursive types, Theory of Computing Systems, 42(3), 2008, 306-348.
• [10] Bakel, S. van, Fern´andez, M.: Normalisation Results for Typeable Rewrite Systems, Information and Computation, 2(133), 1997, 73-116.
• [11] Bakel, S. van, Lengrand, S., Lescanne, P.: The languageX: Circuits, Computations and Classical Logic, Proceedings of Ninth Italian Conference on Theoretical Computer Science (ICTCS'05), Siena, Italy (M. Coppo, E. Lodi, G. M. Pinna, Eds.), 3701, Springer Verlag, 2005.
• [12] Bakel, S. van, Lescanne, P.: Computation with Classical Sequents, Mathematical Structures in Computer Science, 18, 2008, 555-609.
• [13] Barbanera, F., Berardi, S.: A Symmetric Lambda Calculus for Classical Program Extraction, Information and Computation, 125(2), 1996, 103-117.
• [14] Barbanera, F., Dezani-Ciancaglini,M., de'Liguoro, U.: Intersection and Union Types: Syntax and Semantics, Information and Computation, 119(2), 1995, 202-230.
• [15] Barendregt, H.: The Lambda Calculus: its Syntax and Semantics, Revised edition, North-Holland, Amsterdam, 1984.
• [16] Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment, Journal of Symbolic Logic, 48(4), 1983, 931-940.
• [17] Bloo, R., Rose, K.: Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection, CSN'95 - Computer Science in the Netherlands, 1995.
• [18] Church, A.: A Note on the Entscheidungsproblem, Journal of Symbolic Logic, 1(1), 1936, 40-41.
• [19] Coppo, M., Dezani-Ciancaglini, M.: A New Type Assignment for Lambda-Terms, Archive für Mathematischer Logic und Grundlagenforschung, 19, 1978, 139-156.
• [20] Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 27, 1981, 45-58.
• [21] Curien, P.-L., Herbelin, H.: The Duality of Computation, Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), 35.9, ACM, 2000.
• [22] Curry, H., Feys, R.: Combinatory Logic, vol. 1, North-Holland, Amsterdam, 1958.
• [23] Davies, R., Pfenning, F.: A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, 11(4), 2001, 511-540.
• [24] Dougherty,D., Ghilezan, S., Lescanne, P.: Intersection and Union Types in the λμ˜μ-calculus, Electronic Proceedings of 2nd International Workshop Intersection Types and Related Systems (ITRS'04), Turku, Finland, 136, 2004.
• [25] Dougherty, D., Ghilezan, S., Lescanne, P.: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage, Theoretical Computer Science, 398, 2008.
• [26] Dougherty, D., Ghilezan, S., Lescanne, P., Likavec, S.: Strong Normalization of the Dual Classical Sequent Calculus, Proceedings of 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'05), 3835, 2005.
• [27] Dunfield, J., Pfenning, F.: Type Assignment for Intersections and Unions in Call-by-Value Languages, Proceedings of 6th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'03) (A. D. Gordon, Ed.), 2003.
• [28] Gentzen, G.: Investigations into logical deduction, The Collected Papers of Gerhard Gentzen, Ed M. E. Szabo, North Holland, 68ff (1969), 1935.
• [29] Harper, B., Lillibridge,M.: ML with callcc is unsound, 1991, Post to TYPES mailing list, July 8.
• [30] Herbelin, H.: C'est maintenant qu'on calcule: au coeur de la dualité, Mémoire d'habilitation, Université Paris 11, Décembre 2005.
• [31] Hindley, J.: Coppo-Dezani Types do not Correspond to Propositional Logic, Theoretical Computer Science, 28, 1984, 235-236.
• [32] Hindley, J.: Basic Simple Type Theory, Cambridge University Press, 1997.
• [33] Honda, K., Tokoro, M.: An object calculus for asynchronous communication, Proceedings of ECOOP'91, 512, Springer Verlag, 1991.
• [34] Kleene, S.: Introduction to Metamathematics, North Holland, Amsterdam, 1952.
• [35] Krivine, J.-L.: Lambda calculus, types and models, Ellis Horwood, 1993.
• [36] Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, 3rd Workshop on Reduction Strategies in Rewriting and Programming (WRS 2003) (B. Gramlich, S. Lucas, Eds.), 86, Elsevier, 2003.
• [37] Milner, R.: Functions as processes, Mathematical Structures in Computer Science, 2(2), 1992, 269-310.
• [38] Milner, R.: Communicating and Mobile Systems: the π-calculus, Cambridge University Press, 1999.
• [39] Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML, MIT Press, 1990, Revised edition.
• [40] Parigot, M.: An algorithmic interpretation of classical natural deduction, Proceedings of 3rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'92), 624, Springer Verlag, 1992.
• [41] Pierce, B.: Programming with Intersection Types and Bounded Polymorphism, Ph.D. Thesis, Carnegie Mellon University, School of Computer Science, Pitssburgh, 1991, CMU-CS-91-205.
• [42] Summers, A.: Curry-Howard Term Calculi for Gentzen-Style Classical Logic, Ph.D. Thesis, Imperial College London, 2008.
• [43] Urban, C.: Classical Logic and Computation, Ph.D. Thesis, University of Cambridge, October 2000.
• [44] Urban, C., Bierman, G.: Strong normalisation of cut-elimination in classical logic, Fundamenta Informaticae, 45(1,2), 2001, 123-155.
• [45] Wadler, P.: Call-by-Value is Dual to Call-by-Name, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, 2003.
• [46] Wright, A.: Simple imperative polymorphism, Lisp and Symbolic Computation, 8(4), 1995, 343-355.