Document Open Access Logo

Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga

Authors Jonas Kaiser, Brigitte Pientka, Gert Smolka

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.21.pdf
  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Jonas Kaiser
Brigitte Pientka
Gert Smolka

Cite As Get BibTex

Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.21

Abstract

We give three formalisations of a proof of the equivalence of the usual, two-sorted presentation of System F and its single-sorted pure type system (PTS) variant Lambda2. This is established by reducing the typability problem of F to Lambda2 and vice versa. A key challenge is the treatment of variable binding and contextual information. The formalisations all share the same high level proof structure using relations to connect the type systems. They do, however, differ significantly in their representation and manipulation of variables and contextual information. In Coq, we use pure de Bruijn indices and parallel substitutions. In Abella, we use higher-order abstract syntax (HOAS) and nominal constants of the ambient reasoning logic. In Beluga, we also use HOAS but within contextual modal type theory. Our contribution is twofold. First, we present and compare a collection of machine-checked solutions to a non-trivial theoretical result. Second, we propose our proof as a benchmark, complementing the POPLmark and ORBI challenges by testing how well a given proof assistant or framework handles complex contextual information involving multiple type systems.

Subject Classification

Keywords
  • Pure Type Systems
  • System F
  • de Bruijn Syntax
  • Higher-Order Abstract Syntax
  • Contextual Reasoning

Metrics

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

References

  1. Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. JFP, 1(4):375-416, 1991. Google Scholar
  2. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In TPHOL, LNCS 3603, pages 50-65. Springer, 2005. Google Scholar
  3. Brian E. Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In POPL 2008, pages 3-15. ACM, 2008. Google Scholar
  4. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. JFR, 7(2):1-89, 2014. Google Scholar
  5. Henk Barendregt. Introduction to generalized type systems. JFP, 1(2):125-154, 1991. Google Scholar
  6. The Coq proof assistant. URL: http://coq.inria.fr/.
  7. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. Google Scholar
  8. Amy P. Felty and Alberto Momigliano. Hybrid - A definitional two-level approach to reasoning with higher-order abstract syntax. JAR, 48(1):43-105, 2012. Google Scholar
  9. Amy P. Felty, Alberto Momigliano, and Brigitte Pientka. The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2 - a survey. Journal of Automated Reasoning, 55(4):307-372, 2015. Google Scholar
  10. Amy P. Felty and Brigitte Pientka. Reasoning with higher-order abstract syntax and contexts: A comparison. In ITP 2010, LNCS 6172, pages 227-242. Springer, 2010. Google Scholar
  11. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Combining generic judgments with recursive definitions. In Frank Pfenning, editor, LICS 2008. IEEE Computer Society Press, 2008. Google Scholar
  12. Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. JAR, 49(2):241-273, 2012. Google Scholar
  13. Jan Herman Geuvers. Logics and type systems. Proefschrift, Katholieke Univ. Nijmegen, 1993. Google Scholar
  14. Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. Thèse de doctorat d'état, Université Paris VII, 1972. Google Scholar
  15. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge Univ. Press, 1989. Google Scholar
  16. Healfdene Goguen and James McKinna. Candidates for substitution. Technical Report ECS-LFCS-97-358, Univ. of Edinburgh, 1997. Google Scholar
  17. Robert Harper. Practical foundations for programming languages. Cambridge Univ. Press, 2013. Google Scholar
  18. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, January 1993. Google Scholar
  19. Jonas Kaiser, Tobias Tebbi, and Gert Smolka. Equivalence of System F and λ 2 in Coq based on context morphism lemmas. In CPP 2017. ACM, 2017. Google Scholar
  20. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1-49, 2008. Google Scholar
  21. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In PLDI 1988, pages 199-208. ACM, 1988. Google Scholar
  22. Frank Pfenning and Carsten Schürmann. System description: Twelf - A meta-logical framework for deductive systems. In CADE 1999, pages 202-206. Springer, 1999. Google Scholar
  23. Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In POPL 2008, pages 371-382. ACM Press, 2008. Google Scholar
  24. Brigitte Pientka. Beluga: programming with dependent types, contextual data, and contexts. In FLOPS 2010, LNCS 6009, pages 1-12. Springer, 2010. Google Scholar
  25. Brigitte Pientka and Andrew Cave. Inductive Beluga:Programming Proofs (System Description). In CADE 2015, LNCS 9195, pages 272-281. Springer, 2015. Google Scholar
  26. John Charles Reynolds. Towards a theory of type structure. In Paris Colloque sur la Programmation, LNCS 19, pages 408-423. Springer, 1974. Google Scholar
  27. Steven Schäfer, Gert Smolka, and Tobias Tebbi. Completeness and decidability of de Bruijn substitution algebra in Coq. In CPP 2015, pages 67-73. ACM, 2015. Google Scholar
  28. Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In ITP 2015, LNCS 9236, pages 359-374. Springer, 2015. Google Scholar
  29. Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Dep. of Math. Sciences, Carnegie Mellon Univ., 1999. CMU-CS-99-167. 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 About DROPS Imprint Privacy Contact