Typed Applicative Structures and Normalization by Evaluation for System F^ω

1. Abel, A.: Weak βη-normalization and normalization by evaluation for System F. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 497–511. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

2. Abel, A.: Typed applicative structures and normalization by evaluation for System F^ω (full version) (2009), http://www.tcs.ifi.lmu.de/~abel/fomegaNbe.pdf

3. Abel, A., Coquand, T., Dybjer, P.: Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In: LICS 2007, pp. 3–12. IEEE CS Press, Los Alamitos (2007)

   Google Scholar 

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

5. Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.J.: Normalization by evaluation for typed lambda calculus with coproducts. In: LICS 2001, pp. 303–310. IEEE CS Press, Los Alamitos (2001)

   Google Scholar 

6. Altenkirch, T., Hofmann, M., Streicher, T.: Reduction-free normalisation for a polymorphic system. In: LICS 1996, pp. 98–106. IEEE CS Press, Los Alamitos (1996)

   Google Scholar 

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

   MATH  Google Scholar 

8. Barral, F.: Decidability for non-standard conversions in lambda-calculus. PhD thesis, Ludwig-Maximilians-University, Munich (2008)

   Google Scholar 

9. Balat, V., Di Cosmo, R., Fiore, M.P.: Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In: POPL 2004, pp. 64–76. ACM, New York (2004)

   Google Scholar 

10. Bruce, K.B., Meyer, A.R.: The semantics of second order polymorphic lambda calculus. In: Plotkin, G., MacQueen, D.B., Kahn, G. (eds.) Semantics of Data Types 1984. LNCS, vol. 173, pp. 131–144. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

11. Berger, U., Schwichtenberg, H.: An inverse to the evaluation functional for typed λ-calculus. In: LICS 1991, pp. 203–211. IEEE CS Press, Los Alamitos (1991)

    Google Scholar 

12. Chapman, J., Altenkirch, T., McBride, C.: Epigram reloaded: a standalone typechecker for ETT. In: TFP 2005. Trends in Functional Programming, vol. 6, pp. 79–94. Intellect (2007)

    Google Scholar 

13. Coquand, T., Dybjer, P.: Intuitionistic model constructions and normalization proofs. MSCS 7(1), 75–94 (1997)

    MathSciNet  MATH  Google Scholar 

14. Coquand, T.: An algorithm for type-checking dependent types. In: MPC 1995. SCP, vol. 26, pp. 167–177. Elsevier, Amsterdam (1995)

    Google Scholar 

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

    Chapter  Google Scholar 

16. Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. JSL 65(2), 525–549 (2000)

    MathSciNet  MATH  Google Scholar 

17. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002. SIGPLAN Notices, vol. 37, pp. 235–246. ACM, New York (2002)

    Google Scholar 

18. Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in TCS, vol. 7. CUP (1989)

    Google Scholar 

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

20. Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers, Göteborg, Sweden (2007)

    Google Scholar 

21. Pollack, R.: Closure under alpha-conversion. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 313–332. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

22. Seely, R.A.G.: Categorical semantics for higher order polymorphic lambda calculus. JSL 52(4), 969–989 (1987)

    MathSciNet  MATH  Google Scholar 

Download references