Document Open Access Logo

The Delta-calculus: Syntax and Types

Authors Luigi Liquori, Claude Stolze

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.28.pdf
  • Filesize: 0.57 MB
  • 20 pages

Document Identifiers

Author Details

Luigi Liquori
  • Université Côte d'Azur, Inria, Sophia Antipolis, France
Claude Stolze
  • Université Côte d'Azur, Inria, Sophia Antipolis, France

Funding

Work supported by the COST Action CA15123 EUTYPES "The European research network on types for programming and verification".

Acknowledgements

We are grateful to Benjamin Pierce, Joe Wells, Furio Honsell, and the anonymous reviewers for the useful comments and remarks.

Cite AsGet BibTex

Luigi Liquori and Claude Stolze. The Delta-calculus: Syntax and Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.28

Abstract

We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Sallé, the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection typed systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems à la Curry and the corresponding intersection typed systems à la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Type theory
Keywords
  • intersection types
  • lambda calculus à la Church and à la Curry
  • proof-functional logics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theor. Comput. Sci., 355(2):108-126, 2006. Google Scholar
  2. Franco Barbanera and Simone Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, 33:189-211, 1994. Google Scholar
  3. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, revised edition, 1984. Google Scholar
  4. Henk P. Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A Filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931-940, 1983. Google Scholar
  5. Henk P. Barendregt, Wil Dekkers, and Richard Statman. Lambda calculus with types. Cambridge University Press, 2013. Google Scholar
  6. Choukri-Bey Ben-Yelles. Type assignment in the lambda-calculus: syntax and semantics. PhD thesis, University College of Swansea, 1979. Google Scholar
  7. Viviana Bono, Betti Venneri, and Lorenzo Bettini. A typed lambda calculus with intersection types. Theor. Comput. Sci., 398(1-3):95-113, 2008. Google Scholar
  8. Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as Implicit Coercion. Inf. Comput., 93(1):172-221, 1991. Google Scholar
  9. Antonio Bucciarelli, Adolfo Piperno, and Ivano Salvo. Intersection types and λ-definability. Mathematical Structures in Computer Science, 13(1):15-53, 2003. Google Scholar
  10. Beatrice Capitani, Michele Loreti, and Betti Venneri. Hyperformulae, Parallel Deductions and Intersection Types. Proc. of BOTH, Electr. Notes Theor. Comput. Sci., 50(2):180-198, 2001. Google Scholar
  11. Luca Cardelli and Peter Wegner. On Understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471-523, December 1985. Google Scholar
  12. Mario Coppo and Mariangiola Dezani-Ciancaglini. An Extension of the Basic Functionality Theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. Google Scholar
  13. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sallé. Functional characterization of some semantic equalities inside λ-calculus. In International Colloquium on Automata, Languages, and Programming, pages 133-146. Springer-Verlag, 1979. Google Scholar
  14. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 27(2-6):45-58, 1981. Google Scholar
  15. Rowan Davies. Practical Refinement-Type Checking. PhD thesis, Carnegie Mellon University, 2005. CMU-CS-05-110. Google Scholar
  16. Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, and Claude Stolze. A Realizability Interpretation for Intersection and Union Types. In Proc. of APLAS, volume 10017 of Lecture Notes in Computer Science, pages 187-205. Springer-Verlag, 2016. Google Scholar
  17. Daniel J. Dougherty and Luigi Liquori. Logic and Computation in a Lambda Calculus with Intersection and Union Types. In Proc. of LPAR, volume 6355 of Lecture Notes in Computer Science, pages 173-191. Springer-Verlag, 2010. Google Scholar
  18. Andrej Dudenhefner, Moritz Martens, and Jakob Rehof. The Algebraic Intersection Type Unification Problem. Logical Methods in Computer Science, 13(3), 2017. Google Scholar
  19. Joshua Dunfield. Refined typechecking with Stardust. In Proc. of PLPV, pages 21-32, 2007. Google Scholar
  20. Joshua Dunfield. Elaborating intersection and union types. J. Funct. Program., 24(2-3):133-165, 2014. Google Scholar
  21. Timothy S. Freeman and Frank Pfenning. Refinement Types for ML. In Proc. of PLDI, pages 268-277, 1991. Google Scholar
  22. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, 55(4):19, 2008. Google Scholar
  23. Herman Geuvers. The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi. In Proc. of LICS, pages 453-460, 1992. Google Scholar
  24. Robert Harper, Furio Honsell, and Gordon Plotkin. A Framework for Defining Logics. J. ACM, 40(1):143-184, 1993. Google Scholar
  25. J. Roger Hindley. The simple semantics for Coppo-Dezani-Sallé types. In International Symposium on Programming, pages 212-226, 1982. Google Scholar
  26. J. Roger Hindley. Coppo-Dezani types do not correspond to propositional logic. Theor. Comput. Sci., 28:235-236, 1984. Google Scholar
  27. Furio Honsell, Luigi Liquori, Claude Stolze, and Ivan Scagnetto. The Delta-Framework. In Proc of FSTTCS, pages 37:1-37:21, 2018. Google Scholar
  28. Assaf J. Kfoury and Joe B. Wells. Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci., 311(1-3):1-70, 2004. Google Scholar
  29. Luigi Liquori and Simona Ronchi Della Rocca. Towards an intersection typed system à lahurch. Proc. of ITRS, Electronic Notes in Theoretical Computer Science, 136:43-56, 2005. Google Scholar
  30. Luigi Liquori and Simona Ronchi Della Rocca. Intersection Typed System à lahurch. Information and Computation, 9(205):1371-1386, 2007. Google Scholar
  31. Luigi Liquori and Claude Stolze. A Decidable Subtyping Logic for Intersection and Union Types. In Proc of TTCS, volume 10608 of Lecture Notes in Computer Science, pages 74-90. Springer-Verlag, 2017. Google Scholar
  32. Edgar G. K. Lopez-Escobar. Proof functional connectives. In Methods in Mathematical Logic, volume 1130 of Lecture Notes in Mathematics, pages 208-221. Springer-Verlag, 1985. Google Scholar
  33. Grigori Mints. The Completeness of Provable Realizability. Notre Dame Journal of Formal Logic, 30(3):420-441, 1989. Google Scholar
  34. Alexandre Miquel. The Implicit Calculus of Constructions. In Proc. of TLCA, volume 2044 of Lecture Notes in Computer Science, pages 344-359. Springer-Verlag, 2001. Google Scholar
  35. Rob. P. Nederpelt. Strong Normalization in a typed lambda calculus with lambda structured types. PhD thesis, Eindhoven Technological University, 1973. Google Scholar
  36. Benjamin C. Pierce. Programming with intersection types, union types, and bounded polymorphism. PhD thesis, Technical Report CMU-CS-91-205. Carnegie Mellon University, 1991. Google Scholar
  37. Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991. Google Scholar
  38. Elaine Pimentel, Simona Ronchi Della Rocca, and Luca Roversi. Intersection Types from a Proof-theoretic Perspective. Fundam. Inform., 121(1-4):253-274, 2012. Google Scholar
  39. Garrel Pottinger. 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, 1980. Google Scholar
  40. Jakob Rehof and Pawel Urzyczyn. The Complexity of Inhabitation with Explicit Intersection. In Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, pages 256-270, 2012. Google Scholar
  41. John C. Reynolds. Preliminary Design of the Programming Language Forsythe. Report CMU-CS-88-159, Carnegie Mellon University, june 21 1988. Google Scholar
  42. Simona Ronchi Della Rocca and Luca Roversi. Intersection logic. In Proc. of CSL, volume 2142 of Lecture Notes in Computer Science, pages 421-428. Springer-Verlag, 2001. Google Scholar
  43. Claude Stolze, Luigi Liquori, Furio Honsell, and Ivan Scagnetto. Towards a Logical Framework with Intersection and Union Types. In Proc. of LFMTP, pages 1-9, 2017. Google Scholar
  44. Masako Takahashi. Parallel reductions in λ-calculus. Information and computation, 118(1):120-127, 1995. Google Scholar
  45. Pawel Urzyczyn. The Emptiness Problem for Intersection Types. J. Symb. Log., 64(3):1195-1215, 1999. Google Scholar
  46. Steffen van Bakel. Cut-Elimination in the strict intersection type assignment system is strongly normalizing. Notre Dame Journal of Formal Logic, 45(1):35-63, 2004. Google Scholar
  47. Vincent van Oostrom and Femke van Raamsdonk. Weak orthogonality implies confluence: the higher-order case. In Proc. of LFCS, volume 813 of Lecture Notes in Computer Science, pages 379-392. Springer-Verlag, 1994. Google Scholar
  48. Betti Venneri. Intersection Types as Logical Formulae. J. Log. Comput., 4(2):109-124, 1994. Google Scholar
  49. Joe B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Program., 12(3):183-227, 2002. Google Scholar
  50. Joe B. Wells and Christian Haack. Branching Types. In Proc. of ESOP, volume 2305 of Lecture Notes in Computer Science, pages 115-132. Springer-Verlag, 2002. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact