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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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 issue
Altenkirch, T., Chapman, J.: Big step normalisation. Draft, available on the authors’ homepages (2008)
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)
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
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)
Bruce, K.B., Longo, G.: On combinatory algebras and their expansions. Theor. Comput. Sci. 31, 31–40 (1984)
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)
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)
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)
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)
Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundam. Inform. 65(1-2), 113–134 (2005)
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)
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)
Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic 65(2), 525–549 (2000)
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)
H. Goguen.: A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh. Available as LFCS Report ECS-LFCS-94-304 (August 1994)
Harper, R., Pfenning, F.: On equivalence and canonical forms in the LF type theory. ACM Transactions on Computational Logic 6(1), 61–101 (2005)
INRIA. The Coq Proof Assistant, Version 8.1. INRIA (2007), http://coq.inria.fr/
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)
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)
P. Martin-Löf.: Substitution calculus. Lecture in Göteborg (November 1992) (unpublished)
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)
Pitts, A.M.: Alpha-structural recursion and induction. Journal of the ACM 53, 459–506 (2006)
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)
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)
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)
Shinwell, M.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, University of Cambridge (2005)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abel, A., Coquand, T., Dybjer, P. (2008). Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory. In: Audebaud, P., Paulin-Mohring, C. (eds) Mathematics of Program Construction. MPC 2008. Lecture Notes in Computer Science, vol 5133. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70594-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-70594-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70593-2
Online ISBN: 978-3-540-70594-9
eBook Packages: Computer ScienceComputer Science (R0)