Document Open Access Logo

Objects and Subtyping in the Lambda-Pi-Calculus Modulo

Authors Raphaël Cauderlier, Catherine Dubois

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2014.47.pdf
  • Filesize: 0.61 MB
  • 25 pages

Document Identifiers

Author Details

Raphaël Cauderlier
Catherine Dubois

Cite AsGet BibTex

Raphaël Cauderlier and Catherine Dubois. Objects and Subtyping in the Lambda-Pi-Calculus Modulo. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 47-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TYPES.2014.47

Abstract

We present a shallow embedding of the Object Calculus of Abadi and Cardelli in the lambda-Pi-calculus modulo, an extension of the lambda-Pi-calculus with rewriting. This embedding may be used as an example of translation of subtyping. We prove this embedding correct with respect to the operational semantics and the type system of the Object Calculus. We implemented a translation tool from the Object Calculus to Dedukti, a type-checker for the lambda-Pi-calculus modulo.
Keywords
  • object
  • calculus
  • encoding
  • dependent type
  • rewrite system

Metrics

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

References

  1. Martín Abadi and Luca Cardelli. A theory of primitive objects: Untyped and first-order systems. In TACS’94, Theoretical Aspects of Computing Sofware, pages 296-320, 1994. Google Scholar
  2. Martín Abadi and Luca Cardelli. A Theory of Objects. Monographs in Computer Science. Springer New York, 1996. Google Scholar
  3. Ali Assaf and Guillaume Burel. Holide. URL: https://www.rocq.inria.fr/deducteam/Holide/index.html.
  4. Mathieu Boespflug and Guillaume Burel. CoqInE : Translating the calculus of inductive constructions into the λΠ-calculus modulo. In International Workshop on Proof Exchange for Theorem Proving, 2012. Google Scholar
  5. Mathieu Boespflug, Quentin Carbonneaux, and Olivier Hermant. The lambda-pi-calculus modulo as a universal proof language. In International Workshop on Proof Exchange for Theorem Proving, 2012. Google Scholar
  6. Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant, and Ronan Saillard. Dedukti: a universal proof checker. URL: http://dedukti.gforge.inria.fr.
  7. Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. Information and Computation, 155(1/2):108-133, November 1999. Google Scholar
  8. Guillaume Burel. A shallow embedding of resolution and superposition proofs into the λπ-calculus modulo. In International Workshop on Proof Exchange for Theorem Proving, 2013. Google Scholar
  9. Raphaël Cauderlier. Focalide. URL: https://www.rocq.inria.fr/deducteam/Focalide.
  10. Raphaël Cauderlier. Sigmaid. URL: http://sigmaid.gforge.inria.fr.
  11. Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan. Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts. J. Autom. Reason., 39(1):1-47, July 2007. Google Scholar
  12. Horatiu Cirstea, Claude Kirchner, and Luigi Liquori. Matching Power. In Proceedings of RTA'2001, Lecture Notes in Computer Science. Springer-Verlag, May 2001. Google Scholar
  13. Horatiu Cirstea, Luigi Liquori, and Benjamin Wack. Rewriting calculus with fixpoints: Untyped and first-order systems. In TYPES, volume 3085. Springer, 2003. Google Scholar
  14. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and José F. Quesada. Maude: Specification and programming in rewriting logic. Manual distributed as documentation of the Maude system, Computer Science Laboratory, SRI International. http://maude.csl.sri.com/manual, January 1999.
  15. The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
  16. Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. In Simona Ronchi Della Rocca, editor, TLCA, volume 4583 of LNCS, pages 102-117. Springer, 2007. Google Scholar
  17. David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, and Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. In Logic for Programming Artificial Intelligence and Reasoning (LPAR), volume 8312 of LNCS/ARCoSS. Springer, 2013. Google Scholar
  18. Kathleen Fisher, Furio Honsell, and John C. Mitchell. A lambda Calculus of Objects and Method Specialization. Nordic Journal of Computing, 1:3-37, 1994. Google Scholar
  19. J. Nathan Foster and Dimitrios Vytiniotis. A theory of featherweight java in isabelle/hol. Archive of Formal Proofs, March 2006. http://afp.sf.net/entries/FeatherweightJava.shtml, Formal proof development.
  20. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, January 1993. Google Scholar
  21. Michael Hedberg. A coherence theorem for martin-löf’s type theory. J. Functional Programming, pages 4-8, 1998. Google Scholar
  22. Ludovic Henrio and Florian Kammüller. A mechanized model of the theory of objects. In MarcelloM. Bonsangue and EinarBroch Johnsen, editors, Formal Methods for Open Object-Based Distributed Systems, volume 4468 of Lecture Notes in Computer Science, pages 190-205. Springer Berlin Heidelberg, 2007. Google Scholar
  23. Ludovic Henrio, Florian Kammüller, Bianca Lutz, and Henry Sudhof. Locally nameless sigma calculus. Archive of Formal Proofs, April 2010. http://afp.sf.net/entries/Locally-Nameless-Sigma.shtml, Formal proof development.
  24. . Focalize. http://focalize.inria.fr. Google Scholar
  25. Atsushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight java - a minimal core calculus for java and gj. In ACM Transactions on Programming Languages and Systems, pages 132-146, 1999. Google Scholar
  26. Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, and Nicholas Cameron. Encoding featherweight java with assignment and immutability using the coq proof assistant. In Workshop on Formal Techniques for Java-like Programs, FTfJP'12, pages 11-19, New York, NY, USA, 2012. ACM. Google Scholar
  27. Fritz Müller. Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters, 41(6):293-299, 1992. Google Scholar
  28. R. P. Nederpelt, J. H. Geuvers, and R. C. de Vrijer. Selected papers on Automath. Elsevier, Amsterdam, 1994. Google Scholar
  29. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Programming Language Design and Implementation, 1988. Google Scholar
  30. Frank Pfenning and Carsten Schurmann. System description: Twelf - a meta-logical framework for deductive systems. In International Conference on Automated Deduction (CADE-16), pages 202-206. Springer-Verlag LNAI, 1999. Google Scholar
  31. Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207-247, April 1994. Google Scholar
  32. Jan Zwanenburg. Object-Oriented Concepts and Proof Rules: Formalization in Type Theory and Implementation in Yarrow. PhD thesis, Eindhoven University of Technology, 1999. 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