Advertisement

Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

  • Andreas Abel
  • Thierry Coquand
  • Peter Dybjer
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5133)

Abstract

Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of values when checking equalities. Here we analyze a version of Coquand’s algorithm for checking the βη-equality of such semantic values in a theory with a predicative universe hierarchy and large elimination rules. Although this algorithm does not rely on normalization by evaluation explicitly, we show that similar ideas can be employed for its verification. In particular, our proof uses the new notions of contextual reification and strong semantic equality.

The algorithm is part of a bi-directional type checking algorithm which checks whether a normal term has a certain semantic type, a technique used in the proof assistants Agda and Epigram. We work with an abstract notion of semantic domain in order to accommodate a variety of possible implementation techniques, such as normal forms, weak head normal forms, closures, and compiled code. Our aim is to get closer than previous work to verifying the type-checking algorithms which are actually used in practice.

Keywords

Normal Form Inference Rule Type Theory Kripke Model Neutral Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [AAD07]
    Abel, A., Aehlig, K., Dybjer, P.: Normalization by evaluation for Martin-Löf type theory with one universe. In: Fiore, M. (ed.) Proc. of the 23rd Conf. on the Mathematical Foundations of Programming Semantics (MFPS XXIII). Electr. Notes in Theor. Comp. Sci, vol. 173, pp. 17–39. Elsevier, Amsterdam (2007)Google Scholar
  2. [AC07]
    Abel, A., Coquand, T.: Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. Fundam. Inform. 77(4), 345–395 (2005); TLCA 2005 special issueMathSciNetGoogle Scholar
  3. [AC08]
    Altenkirch, T., Chapman, J.: Big step normalisation. Draft, available on the authors’ homepages (2008)Google Scholar
  4. [ACD07]
    Abel, A., Coquand, T., Dybjer, P.: Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In: Proc. of the 22nd IEEE Symp. on Logic in Computer Science (LICS 2007), pp. 3–12. IEEE Computer Soc. Press, Los Alamitos (2007)Google Scholar
  5. [ACD08]
    Abel, A., Coquand, T., Dybjer, P.: A semantic βη-equality algorithm for Martin-Löf Type Theory (extended version). Technical report, Ludwig-Maximilians-University Munich (2008), http://www.tcs.ifi.lmu.de/~abel/semEqTR.pdf
  6. [Bar84]
    Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)zbMATHGoogle Scholar
  7. [BL84]
    Bruce, K.B., Longo, G.: On combinatory algebras and their expansions. Theor. Comput. Sci. 31, 31–40 (1984)zbMATHCrossRefMathSciNetGoogle Scholar
  8. [BS91]
    Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed λ-calculus. In: Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, Amsterdam, pp. 203–211 (July 1991)Google Scholar
  9. [CAM07]
    Chapman, J., Altenkirch, T., McBride, C.: Epigram reloaded: a standalone typechecker for ETT. In: van Eekelen, M.C.J.D. (ed.) Revised Selected Papers from the 6th Symp. on Trends in Functional Programming, TFP 2005, Trends in Functional Programming, Intellect, vol. 6, pp. 79–94 (2007)Google Scholar
  10. [Coq94]
    Coquand, C.: From semantics to rules: A machine assisted analysis. In: Meinke, K., Börger, E., Gurevich, Y. (eds.) Proc. of the 7th Wksh. on Computer Science Logic, CSL 1993. LNCS, vol. 832, pp. 91–105. Springer, Heidelberg (1994)Google Scholar
  11. [Coq96]
    Coquand, T.: An algorithm for type-checking dependent types. In: Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction, Kloster Irsee, Germany, July 17–21, 1995. Science of Computer Programming, vol. 26, pp. 167–177. Elsevier Science, Amsterdam (1996)Google Scholar
  12. [CPT05]
    Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundam. Inform. 65(1-2), 113–134 (2005)zbMATHMathSciNetGoogle Scholar
  13. [Dan99]
    Danvy, O.: Type-directed partial evaluation. In: Hatcliff, J., Mogensen, T.Æ., Thiemann, P. (eds.) Partial Evaluation – Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998. LNCS, vol. 1706, pp. 367–411. Springer, Heidelberg (1999)Google Scholar
  14. [Dyb96]
    Dybjer, P.: Internal type theory. In: Berardi, S., Coppo, M. (eds.) Types for Proofs and Programs (TYPES 1995). LNCS, vol. 1158, pp. 120–134. Springer, Heidelberg (1996)Google Scholar
  15. [Dyb00]
    Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic 65(2), 525–549 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  16. [GL02]
    Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proc. of the 7th ACM SIGPLAN Int. Conf. on Functional Programming (ICFP 2002). SIGPLAN Notices, vol. 37, pp. 235–246. ACM Press, New York (2002)CrossRefGoogle Scholar
  17. [Gog94]
    H. Goguen.: A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh. Available as LFCS Report ECS-LFCS-94-304 (August 1994)Google Scholar
  18. [HP05]
    Harper, R., Pfenning, F.: On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic 6(1), 61–101 (2005)CrossRefMathSciNetGoogle Scholar
  19. [INR07]
    INRIA. The Coq Proof Assistant, Version 8.1. INRIA (2007), http://coq.inria.fr/
  20. [Ler06]
    Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proc. of the 33rd ACM Symp. on Principles of Programming Languages, POPL 2006, pp. 42–54. ACM Press, New York (2006)Google Scholar
  21. [ML75]
    Martin-Löf, P.: About models for intuitionistic type theories and the notion of definitional equality. In: Kanger, S. (ed.) Proceedings of the 3rd Scandinavian Logic Symposium, pp. 81–109 (1975)Google Scholar
  22. [ML92]
    P. Martin-Löf.: Substitution calculus. Lecture in Göteborg (November 1992) (unpublished)Google Scholar
  23. [Nor07]
    Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-41296 Göteborg, Sweden (September 2007)Google Scholar
  24. [Pit06]
    Pitts, A.M.: Alpha-structural recursion and induction. Journal of the ACM 53, 459–506 (2006)CrossRefMathSciNetGoogle Scholar
  25. [Pol94]
    Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) Types for Proofs and Programs: International Workshop. LNCS, vol. 806, pp. 313–332. Springer, Heidelberg (1994)Google Scholar
  26. [PS99]
    Pfenning, F., Schürmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) Proceedings of the 16th International Conference on Automated Deduction (CADE-16). LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)Google Scholar
  27. [PT98]
    Pierce, B.C., Turner, D.N.: Local type inference. In: POPL 98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, California (1998)Google Scholar
  28. [Shi05]
    Shinwell, M.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, University of Cambridge (2005)Google Scholar
  29. [SS08]
    Schürmann, C., Sarnat, J.: Structural logical relations. In: Pfenning, F. (ed.) Proc. of the 23nd IEEE Symp. on Logic in Computer Science (LICS 2008) (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Andreas Abel
    • 1
  • Thierry Coquand
    • 2
  • Peter Dybjer
    • 2
  1. 1.Department of Computer ScienceLudwig-Maximilians-UniversityMunich 
  2. 2.Department of Computer ScienceChalmers University of Technology 

Personalised recommendations