Weak βη-Normalization and Normalization by Evaluation for System F

1. 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 

2. Abel, A., Coquand, T., Dybjer, P.: Verifying a semantic βη-conversion test for martin-löf type theory. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 29–56. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

3. Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.J.: Normalization by evaluation for typed lambda calculus with coproducts. In: Proc. of the 16th IEEE Symp. on Logic in Computer Science (LICS 2001), pp. 303–310. IEEE Computer Soc. Press, Los Alamitos (2001)

   Google Scholar 

4. Altenkirch, T., Hofmann, M., Streicher, T.: Reduction-free normalisation for a polymorphic system. In: Proc. of the 11th IEEE Symp. on Logic in Computer Science (LICS 1996), pp. 98–106. IEEE Computer Soc. Press, Los Alamitos (1996)

   Google Scholar 

5. Altenkirch, T., Hofmann, M., Streicher, T.: Reduction-free normalisation for System F (1997), http://www.cs.nott.ac.uk/~txa/publ/f97.pdf

6. Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam (1984)

   MATH  Google Scholar 

7. Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed λ-calculus. In: Proc. of the 6th IEEE Symp. on Logic in Computer Science (LICS 1991), pp. 203–211. IEEE Computer Soc. Press, Los Alamitos (1991)

   Google Scholar 

8. Blanqui, F.: Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science 15, 37–92 (2005)

   Article  MathSciNet  MATH  Google Scholar 

9. Blanqui, F., Jouannaud, J.-P., Strub, P.-Y.: Building decision procedures in the calculus of inductive constructions. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 328–342. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

10. Chrząszcz, J., Walukiewicz-Chrząszcz, D.: Towards rewriting in coq. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol. 4600, pp. 113–131. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

11. Constable, R.: Team: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)

    Google Scholar 

12. Danvy, O.: Type-directed partial evaluation. In: Hatcliff, J., Mogensen, T.Æ., Thiemann, P. (eds.) DIKU 1998. LNCS, vol. 1706, pp. 367–411. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

13. Debray, S.K., Warren, D.S.: Automatic mode inference for logic programs. Journal of Logic Programming 5, 207–229 (1988)

    Article  MathSciNet  MATH  Google Scholar 

14. Filinski, A.: A semantic account of type-directed partial evaluation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 378–395. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

15. Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)

    MATH  Google Scholar 

16. INRIA: The Coq Proof Assistant, Version 8.1. INRIA (2007), http://coq.inria.fr/

17. Jay, B.: Long βη normal forms and confluence. Technical Report ECS-LFCS-91-183, University of Edinburgh (1991)

    Google Scholar 

18. Matthes, R.: Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. thesis, Ludwig-Maximilians-University (1998)

    Google Scholar 

19. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden (2007)

    Google Scholar 

20. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

21. Pollack, R.: The Theory of LEGO. Ph.D. thesis, University of Edinburgh (1994)

    Google Scholar 

22. Streicher, T.: Semantics of Type Theory. Progress in Theoretical Computer Science. Birkhaeuser Verlag, Basel (1991)

    Book  MATH  Google Scholar 

23. Vaux, L.: A type system with implicit types, English version of his mémoire de maîtrise (2004)

    Google Scholar 

Download references