Conversion by Evaluation

1. Aehlig, K., Haftmann, F., Nipkow, T.: A Compiled Implementation of Normalization by Evaluation. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 39–54. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

2. Altenkirch, T., Dybjer, P., Hofmann, M., Scott, P.: Normalization by evaluation for typed lambda calculus with coproducts. In: Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp. 203–210 (2001)

   Google Scholar 

3. Berger, U., Eberl, M., Schwichtenberg, H.: Normalization by evaluation. Prospects for Hardware Foundations, 117–137 (1998)

   Google Scholar 

4. Berger, U., Eberl, M., Schwichtenberg, H.: Term rewriting for normalization by evaluation. Information and Computation 183(1), 19–42 (2003)

   Article  MATH  MathSciNet  Google Scholar 

5. Blanqui, F., Hardin, T., Weis, P.: On the Implementation of Construction Functions for Non-free Concrete Data Types. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 95–109. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

6. Boespflug, M.: From self-interpreters to normalization by evaluation. In: Informal proceedings of the 2009 Workshop on Normalization by Evaluation, August 2009, pp. 35–38 (2009)

   Google Scholar 

7. Coquand, T., Dybjer, P.: Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science 7(01), 75–94 (1997)

   Article  MATH  MathSciNet  Google Scholar 

8. Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-Pi-calculus modulo. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102–117. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

9. Crégut, P.: Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation 20(3), 209–230 (2007)

   Article  MATH  Google Scholar 

10. Danvy, O.: Type-directed partial evaluation. In: POPL 1996, pp. 242–257 (1996)

    Google Scholar 

11. Filinski, A., Rohde, H.: A denotational account of untyped normalization by evaluation (2004)

    Google Scholar 

12. Gonthier, G.: The four colour theorem: Engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

13. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, pp. 235–246 (2002)

    Google Scholar 

14. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 98–113. Springer, Heidelberg (2005)

    Google Scholar 

15. Le Fessant, F., Maranget, L.: Optimizing pattern matching. In: Proceedings of the sixth ACM SIGPLAN international conference on Functional programming, pp. 26–37 (2001)

    Google Scholar 

16. Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Tech. rep., INRIA (1990)

    Google Scholar 

17. Lévy, J.: Réductions correctes et optimales dans le Lambda-Calcul. Université Paris 7 (1978)

    Google Scholar 

18. Lindley, S.: Normalisation by evaluation in the compilation of typed functional programming languages (2005)

    Google Scholar 

19. Marlow, S., Peyton-Jones, S.: Making a fast curry: push/enter vs. eval/apply for higher-order languages. Journal of Functional Programming 16(4-5), 415–449 (2006)

    Article  MATH  MathSciNet  Google Scholar 

Download references