Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Types for Proofs and Programs

TYPES 1996: Types for Proofs and Programs pp 294–316Cite as

Dependent types with explicit substitutions: A meta-theoretical development

  • Conference paper
  • First Online:

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

Abstract

We present a theory of dependent types with explicit substitutions. We follow a meta-theoretical approach where open expressions —expressions with meta-variables— are first-class objects. The system enjoys properties like type uniqueness, subject reduction, soundness, confluence and weak normalization.

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. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitution. Journal of Functional Programming, 1(4):375–416, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  2. R. Bloo. Manuscript, 1997.

    Google Scholar 

  3. R. Bloo, F. Kamareddine, and R. Nederpelt. The Barendregt cube with definitions and generalised reduction. Information and Computation, 126(2):123–143, 1 May 1996.

    Article  MATH  MathSciNet  Google Scholar 

  4. R. Di Cosmo and D. Kesner. Strong normalization of explicit substitutions via cut elimination in proof nets. In To appear in the Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97) Warsaw, Poland, July 1997.

    Google Scholar 

  5. P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, March 1996.

    Article  MATH  MathSciNet  Google Scholar 

  6. G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 366–374, San Diego, California, 26–29 June 1995. IEEE Computer Society Press.

    Google Scholar 

  7. G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, Bonn, Germany, September 1996. MIT Press. To appear.

    Google Scholar 

  8. H. Geuvers. The Church-Rosser property for βη-reduction in typed λ-calculi. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 453–460, Santa Cruz, California, 22–25 June 1992. IEEE Computer Society Press.

    Google Scholar 

  9. H. Geuvers. A short and flexible proof of Strong Normalization for the Calculus of Constructions. In P. Dybjer and B. Nordström, editors, Types for Proofs and Programs, International Workshop TYPES'94, volume 996 of LNCS, pages 14–38. Båstad, Sweden, 1994. Springer.

    Google Scholar 

  10. H. Geuvers and B. Werner. On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 320–329, Paris, France, 4–7 July 1994. IEEE Computer Society Press.

    Google Scholar 

  11. J. Goubault-Larrecq. Une preuve de terminaison faible du λσ-calcul. Technical Report RR-3090, Unité de recherche INRIA-Rocquencourt, Janvier 1997.

    Google Scholar 

  12. R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143–184, 1993.

    MATH  MathSciNet  Google Scholar 

  13. G. Huet. Confluent reductions. Abstract properties and applications to term rewriting systems. J.A.C.M., 27(4), October 1980.

    Google Scholar 

  14. F. Kamareddine and A. Ríos. The λ∫-calculus: its typed and its extended versions. manuscript, June 1995.

    Google Scholar 

  15. D. Kapur, P. Narendran, F. Otto. On ground-confluence of term rewriting systems. Information and Computation, 86(1):14–31, May 1990.

    Article  MATH  MathSciNet  Google Scholar 

  16. D. Kapur and H. Zhang. RRL: A rewrite rule laboratory-user's manual. Technical Report 89-03, Department of Computer Science, The University of Iowa, 1989.

    Google Scholar 

  17. C. Kirchner and C. Ringeissen. Higher order equational unification via explicit substitutions. In Proceedings International Conference PLILP/ALP/HOA'97, Southampton (England), September 1997. Lecture Notes in Computer Science. Springer-Verlag.

    Google Scholar 

  18. J.-W. Klop. Combinatory reduction systems. Mathematical Center Tracts, (27), 1980.

    Google Scholar 

  19. P. Lescanne. From λσ to λv a journey through calculi of explicit substitutions. In Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 60–69, January 1994.

    Google Scholar 

  20. L. Magnusson. The Implementation of ALF—A Proof Editor Based on Martin-Löf's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers University of Technology and Göteborg University, January 1995.

    Google Scholar 

  21. P.-A. Melliès. Typed λ-calculi with explicit substitutions may not terminate. In Typed Lambda Calculi and Applications, number 902 in LNCS. Second International Conference TLCA'95, Springer-Verlag, 1995.

    Google Scholar 

  22. C. Muñoz. Proof representation in type theory: State of the art. In Proceedings, XXII Latinamerican Conference of Informatics CLEI Panel 96, Santafé de Bogotá, Colombia, June 1996.

    Google Scholar 

  23. C. Muñoz. A left-linear variant of λσ. In Proceedings International Conference PLILP/ALP/HOA'97, Southampton (England), September 1997. Lecture Notes in Computer Science. Springer-Verlag.

    Google Scholar 

  24. G. Nadathur. The (SCons) rule. Personal communication, 1996.

    Google Scholar 

  25. B. Pagano. Confluent extensions of λ⇑. Personal communication, 1996.

    Google Scholar 

  26. A. Ríos. Contributions à l'étude de λ-calculs avec des substitutions explicites. PhD thesis, U. Paris VII, 1993.

    Google Scholar 

  27. E. Ritter. Categorical abstract machines for higher-order lambda calculi. Theoretical Computer Science, 136(1):125–162, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  28. M. Schmidt-Schauss, Computational aspects of an order-sorted logic with term declarations, volume 395 of Lecture Notes in Computer Science and Lecture Notes in Artificial Intelligence. Springer-Verlag Inc., New York, NY, USA, 1989.

    Google Scholar 

  29. P. Severi. Normalisation in LAMBDA CALCULUS and its relation to type inference. PhD thesis, Eindhoven University of Technology, 1996.

    Google Scholar 

  30. A. Tasistro. Formulation of Martin-Löf's theory of types with explicit substitution. Technical report, Chalmers University of Technology, University of Göteborg, Göteborg, Sweden, May 1993.

    Google Scholar 

  31. B. Werner. Une Théorie des Constructions Inductives. PhD thesis, U. Paris VII, 1994.

    Google Scholar 

  32. H. Yokouchi and T. Hikita. A rewriting system for categorical combinators with multiple arguments. SIAM Journal of Computing, 19(1):78–97, February 1990.

    Article  MATH  MathSciNet  Google Scholar 

  33. H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24:89–105, 1995.

    MATH  MathSciNet  Google Scholar 

  34. H. Zantema. Termination of ϕ and Π φ by semantic labelling. Personal communication, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Rocquencourt, B.P. 105, 78153, Le Chesnay Cedex, France

    César Muñoz

Authors
  1. César Muñoz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eduardo Giménez Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Muñoz, C. (1998). Dependent types with explicit substitutions: A meta-theoretical development. In: Giménez, E., Paulin-Mohring, C. (eds) Types for Proofs and Programs. TYPES 1996. Lecture Notes in Computer Science, vol 1512. Springer, Berlin, Heidelberg . https://doi.org/10.1007/BFb0097798

Download citation

  • DOI: https://doi.org/10.1007/BFb0097798

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65137-6

  • Online ISBN: 978-3-540-49562-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation