Document Open Access Logo

The Delta-Framework

Authors Furio Honsell, Luigi Liquori, Claude Stolze, Ivan Scagnetto

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.37.pdf
  • Filesize: 0.58 MB
  • 21 pages

Document Identifiers

Author Details

Furio Honsell
  • Dept. of Mathematics, Computer Science and Physics, University of Udine, Via delle Scienze, 206, 33100 Udine, Italy
Luigi Liquori
  • Université Côte d'Azur, INRIA Sophia Antipolis - Méditerranée 2004 Route des Lucioles - BP 93 FR-06902 Sophia Antipolis, France
Claude Stolze
  • Université Côte d'Azur, INRIA Sophia Antipolis - Méditerranée 2004 Route des Lucioles - BP 93 FR-06902 Sophia Antipolis, France
Ivan Scagnetto
  • Dept. of Mathematics, Computer Science and Physics, University of Udine, Via delle Scienze, 206, 33100 Udine, Italy

Cite AsGet BibTex

Furio Honsell, Luigi Liquori, Claude Stolze, and Ivan Scagnetto. The Delta-Framework. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSTTCS.2018.37

Abstract

We introduce the Delta-framework, LF_Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subtyping, LF_Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF_Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Logic of programs
  • type theory
  • lambda-calculus

Metrics

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

References

  1. Samson Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51(1):1-77, 1991. Google Scholar
  2. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science, 8(1), 2012. Google Scholar
  3. Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and union types: syntax and semantics. Inf. Comput., 119(2):202-230, 1995. Google Scholar
  4. Franco Barbanera and Simone Martini. Proof-functional connectives and realizability. Archive for Mathematical Logic, 33:189-211, 1994. Google Scholar
  5. Henk 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
  6. Gilles Barthe and Olivier Pons. Type Isomorphisms and Proof Reuse in Dependent Type Theory. In Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001, pages 57-71, 2001. Google Scholar
  7. Stefano Berardi. Towards a mathematical analysis of the Coquand–Huet calculus of constructions and the other systems in Barendregt’s cube. PhD thesis, Dipartimento Matematica, Universita di Torino, 1988. Google Scholar
  8. Jan Bessai. Extracting a formally verified Subtyping Algorithm for Intersection Types from Ideals and Filters. Talk at COST Types, 2016. Google Scholar
  9. Olivier Boite. Proof Reuse with Extended Inductive Types. In Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, pages 50-65, 2004. Google Scholar
  10. 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
  11. Beatrice Capitani, Michele Loreti, and Betti Venneri. Hyperformulae, Parallel Deductions and Intersection Types. BOTH, Electr. Notes Theor. Comput. Sci., 50(2):180-198, 2001. Google Scholar
  12. Joshua E. Caplan and Mehdi T. Harandi. A Logical Framework for Software Proof Reuse. In SSR, pages 106-113, 1995. Google Scholar
  13. Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for λ-terms. Arch. Math. Log., 19(1):139-156, 1978. Google Scholar
  14. Mario Coppo, Mariangiola Dezani-Ciancaglini, Honsell Furio, and Longo Giuseppe. Extended Type Structures and Filter Lambda Models. In Logic Colloquium, pages 241-262, 1983. Google Scholar
  15. 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
  16. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Zietschrift für Mathematische Logik und Grundlagen der Mathematik, 27(2-6):45-58, 1981. Google Scholar
  17. Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, and Claude Stolze. A Realizability Interpretation for Intersection and Union Types. In APLAS, volume 10017 of Lecture Notes in Computer Science, pages 187-205. Springer-Verlag, 2016. Google Scholar
  18. Daniel J. Dougherty and Luigi Liquori. Logic and Computation in a Lambda Calculus with Intersection and Union Types. In LPAR, volume 6355 of Lecture Notes in Computer Science, pages 173-191. Springer-Verlag, 2010. Google Scholar
  19. Joshua Dunfield. Elaborating intersection and union types. J. Funct. Program., 24(2-3):133-165, 2014. Google Scholar
  20. Amy P. Felty and Douglas J. Howe. Generalization and Reuse of Tactic Proofs. In Proc. of Logic Programming and Automated Reasoning, 5th International Conference, LPAR, pages 1-15, 1994. Google Scholar
  21. Alain Frisch, Giuseppe Castagna, and Véronique Benzaken. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM (JACM), 55(4):19, 2008. Google Scholar
  22. Robert Harper, Furio Honsell, and Gordon Plotkin. A Framework for Defining Logics. J. ACM, 40(1):143-184, 1993. Google Scholar
  23. Robert Harper and Daniel R. Licata. Mechanizing metatheory in a logical framework. J. Funct. Program., 17(4-5):613-673, 2007. Google Scholar
  24. J. Roger Hindley. The simple semantics for Coppo-Dezani-Sallé types. In International Symposium on Programming, pages 212-226, 1982. Google Scholar
  25. Furio Honsell and Marina Lenisa. Semantical Analysis of Perpetual Strategies in lambda-Calculus. Theor. Comput. Sci., 212(1-2):183-209, 1999. Google Scholar
  26. Furio Honsell, Marina Lenisa, Luigi Liquori, and Ivan Scagnetto. Implementing Cantor’s Paradise. In Proc. of Programming Languages and Systems - 14th Asian Symposium, APLAS, pages 229-250, 2016. Google Scholar
  27. Alexei Kopylov. Dependent intersection: a new way of defining records in type theory. In Proc. of 18th Annual IEEE Symposium of Logic in Computer Science, LICS, pages 86-95, 2003. Google Scholar
  28. Luigi Liquori, Andreas Nuyts, and Claude Stolze. Privates communications, 2017. Google Scholar
  29. Luigi Liquori and Simona Ronchi Della Rocca. Intersection Typed System à lahurch. Information and Computation, 9(205):1371-1386, 2007. Google Scholar
  30. 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
  31. Luigi Liquori and Claude Stolze. The Delta-calculus: syntax and types. Research report, Inria, July 2018. URL: https://arxiv.org/abs/1803.09660.
  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. David B. MacQueen, Gordon D. Plotkin, and Ravi Sethi. An Ideal Model for Recursive Polymorphic Types. Information and Control, 71(1/2):95-130, 1986. Google Scholar
  34. Robert K Meyer and Richard Routley. Algebraic analysis of entailment I. Logique et Analyse, 15:407-428, 1972. Google Scholar
  35. Grigori Mints. The Completeness of Provable Realizability. Notre Dame Journal of Formal Logic, 30(3):420-441, 1989. Google Scholar
  36. Alexandre Miquel. The Implicit Calculus of Constructions. In TLCA, pages 344-359, 2001. Google Scholar
  37. Frank Pfenning. Refinement Types for Logical Frameworks. In TYPES, pages 285-299, 1993. Google Scholar
  38. 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
  39. 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
  40. 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
  41. John C. Reynolds. Preliminary Design of the Programming Language Forsythe. Report CMU-CS-88-159, Carnegie Mellon University, 1988. Google Scholar
  42. Simona Ronchi Della Rocca and Luca Roversi. Intersection logic. In CSL, volume 2142 of Lecture Notes in Computer Science, pages 421-428. Springer-Verlag, 2001. Google Scholar
  43. Vincent Siles and Hugo Herbelin. Equality Is Typable in Semi-full Pure Type Systems. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS, pages 21-30, 2010. Google Scholar
  44. Claude Stolze. Δ-framework implementation. https://github.com/cstolze/Bull and https://github.com/cstolze/Bull-Subtyping, 2017.
  45. Claude Stolze, Luigi Liquori, Furio Honsell, and Ivan Scagnetto. Towards a Logical Framework with Intersection and Union Types. In 11th International Workshop on Logical Frameworks and Meta-languages, LFMTP, pages 1-9, 2017. Google Scholar
  46. Aaron Stump. From realizability to induction via dependent intersection. Annals of Pure and Applied Logic, 169(7):637-655, 2018. Google Scholar
  47. Betti Venneri. Intersection Types as Logical Formulae. J. Log. Comput., 4(2):109-124, 1994. Google Scholar
  48. 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
  49. Joe B. Wells and Christian Haack. Branching Types. In ESOP, volume 2305 of Lecture Notes in Computer Science, pages 115-132. Springer-Verlag, 2002. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact