Document Open Access Logo

Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting

Author Ali Assaf

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.31.pdf
  • Filesize: 457 kB
  • 14 pages

Document Identifiers

Author Details

Ali Assaf

Cite As Get BibTex

Ali Assaf. Conservativity of Embeddings in the lambda Pi Calculus Modulo Rewriting. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 31-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.31

Abstract

The lambda Pi calculus can be extended with rewrite rules to embed
any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing.

Subject Classification

Keywords
  • lambda Pi calculus modulo rewriting
  • pure type systems
  • logical framework
  • normalization
  • conservativit

Metrics

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

References

  1. H. P. Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992. Google Scholar
  2. Gilles Barthe, John Hatcliff, and Morten Heine Sørensen. Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theoretical Computer Science, 269(1-2):317-361, 2001. Google Scholar
  3. Frédéric Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(01):37-92, 2005. Google Scholar
  4. M. Boespflug and G. Burel. CoqInE: translating the calculus of inductive constructions into the λΠ-calculus modulo. In Proof Exchange for Theorem Proving - Second International Workshop, PxTP 2012, pages 44-50, 2012. Google Scholar
  5. M. Boespflug, Q. Carbonneaux, and O. Hermant. The λΠ-calculus modulo as a universal proof language. In Proof Exchange for Theorem Proving - Second International Workshop, PxTP 2012, pages 28-43, 2012. Google Scholar
  6. Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-Pi-calculus modulo. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications, number 4583 in Lecture Notes in Computer Science, pages 102-117. Springer Berlin Heidelberg, 2007. Google Scholar
  7. Gilles Dowek. Models and termination of proof-reduction in the λΠ-calculus modulo theory. arXiv:1501.06522, hal-01101834, 2014. Google Scholar
  8. Herman Geuvers. Logics and type systems. PhD thesis, University of Nijmegen, 1993. Google Scholar
  9. Jean-Yves Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse de doctorat, Université Paris VII, 1972. Google Scholar
  10. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. J. ACM, 40(1):143endash184, 1993. Google Scholar
  11. Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, Inc., New York, NY, USA, 1994. Google Scholar
  12. Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis Naples, 1984. Google Scholar
  13. Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf’s type theory, volume 200. Oxford University Press Oxford, 1990. Google Scholar
  14. Erik Palmgren. On universes in type theory. In Twenty-five years of constructive type theory, pages 191-204. Oxford University Press, 1998. Google Scholar
  15. Cody Roux and Floris van Doorn. The structural theory of pure type systems. In Gilles Dowek, editor, Rewriting and Typed Lambda Calculi, number 8560 in Lecture Notes in Computer Science, pages 364-378. Springer International Publishing, 2014. Google Scholar
  16. Paula Severi. Pure type systems without the Pi-condition. Proceedings of 7th Nordic Workshop on Programming Theory, 1995. Google Scholar
  17. Paula Severi and Erik Poll. Pure type systems with definitions. In Anil Nerode and Yu V. Matiyasevich, editors, Logical Foundations of Computer Science, number 813 in Lecture Notes in Computer Science, pages 316-328. Springer Berlin Heidelberg, 1994. Google Scholar
  18. W. W. Tait. Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic, 32(2):198-212, 1967. 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