Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 1994: Types for Proofs and Programs pp 183–202Cite as

Formalization of a λ-calculus with explicit substitutions in Coq

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 996))

Abstract

We present a formalization of the λσ ⇑-calculus[9] in the Coq V5.8 system[6]. The principal axiomatized result is the confluence of this calculus. Furthermore we propose a uniform encoding for many-sorted first order term rewriting systems, on which we study the local confluence by critical pairs analysis.

This research was partially supported by ESPRIT Basic Research Action “TYPES.”

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. T. Altenkirch, A formalization of the strong normalization proof for System F in LEGO, In Proceedings of the international conference on Typed Lambda Calculi and Applications, TLCA'93, Springer-Verlag, LNCS 664, March 1993.

    Google Scholar 

  2. M. Abadi, L. Cardelli, P.-L. Curien, J.-J. Lévy, Explicit Substitutions, ACM Conference on Principle of Programming Languages, San Francisco, 1990.

    Google Scholar 

  3. T. Coquand, Une théorie des constructions, Thèse de troisième cycle. Université Paris 7. 1985

    Google Scholar 

  4. C. Cornes Inversion des prédicats inductifs, Rapport de stage de DEA d'Informatique Fondamentale, Université Paris VII, septembre 93.

    Google Scholar 

  5. P.-L. Curien, T. Hardin, J.-J. Lévy, Confluence properties of Weak and Strong Calculi of Explicit Substitutions, Rapport de recherche CEDRIC 92-1, 56 pages.

    Google Scholar 

  6. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, B. Werner, The Coq Proof Assistant User's Guide, version 5.8, Rapport technique INRIA 154, Mai 1993.

    Google Scholar 

  7. T. Hardin, Eta-conversion for the languages of explicit substitutions, Applicable Algebra in Engineering, Communication and Computing, 1993.

    Google Scholar 

  8. T. Hardin, J.-J. Lévy, A Confluent Calculus of Substitutions, France-Japan Artificial Intelligence and Computer Science Symposium, Izu, 1989. Rapport de recherche CEDRIC 90/11.

    Google Scholar 

  9. G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,J.A.C.M., vol 27(4), pp 797–821, October 1980.

    Google Scholar 

  10. G. Huet, Inductive Principles Formalized in the Calculus of Constructions, Proceeding of the First Franco-Japanese Symposium on Programming of Future Generation Computers, Tokyo, October 88.

    Google Scholar 

  11. G. Huet, Residual Theory in λ-calculus: A complete Gallina Development, Rapport de recherche INRIA 2002, 1993.

    Google Scholar 

  12. J. McKinna and R. Pollack, Pure Type Systems Formalized, In Proceedings of the international conference on Typed Lambda Calculi and Applications, TLCA'93, Springer-Verlag, LNCS 664, March 1993.

    Google Scholar 

  13. C. Paulin-Mohring, Inductive Definitions in the System Coq-Rules and Properties, Proceedings TLCA 93, Ultrecht, March 93. LNCS 664, p 328–345.

    Google Scholar 

  14. H. Yokouchi, Relationship between λ-calculus and Rewriting Systems for Categorical Combinators, Theoretical Computer Sc. 65, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Projet COQ, INRIA-Rocquencourt, B.P. 105, 78153, Le Chesnay Cedex

    Amokrane Saïbi

Authors
  1. Amokrane Saïbi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Peter Dybjer Bengt Nordström Jan Smith

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Saïbi, A. (1995). Formalization of a λ-calculus with explicit substitutions in Coq. In: Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1994. Lecture Notes in Computer Science, vol 996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60579-7_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-60579-7_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60579-9

  • Online ISBN: 978-3-540-47770-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation