Normalization by evaluation

• Intuitionistic model constructions and normalization proofs (with Thierry Coquand). Proceedings of the 1993 TYPES Workshop, Nijmegen.
• Intuitionistic model constructions and normalization proofs (with Thierry Coquand). Mathematical Structures in Computer Science (1997), vol 7, pp 75-94. Journal version of the above paper with the same title.
• Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids (with Ilya Beylin). pp 47-61 in TYPES '95, LNCS 1158, 1996.
• A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem (with Sten Agerholm and Ilya Beylin), pp 17-32 in Theorem Proving in Higher Order Logics, editors J. von Wright, J. Grundy, J. Harrison, LNCS 1125, August 1996.
• Normalization and the Yoneda embedding. (with Djordje Cubric and Phil Scott). Mathematical Structures in Computer Science (1998), vol 8, pp 153-192.
• Normalization by evaluation for typed lambda calculus with coproducts (with Thorsten Altenkirch, Martin Hofmann, and Phil Scott). Pages 203-210 in Proceedings of 16th Annual Symposium on Logic in Computer Science, June 2001.
• Normalization and Partial Evaluation (with Andrzej Filinski). In Applied Semantics, Advanced Lectures, LNCS 2395, 2002. Tutorial notes from the International Summer School, Caminha, Portugal, September 2000.
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe (with Andreas Abel and Klaus Aehlig). Pages 17-40 in Mathematical Foundations of Programming Semantics, New Orleans, LA, USA, April 2007. Volume 173 in Electronic Notes in Theoretical Computer Science, Elsevier.
• Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements (with Andreas Abel and Thierry Coquand). Proceedings of 22nd IEEE Annual Symposium on Logic in Computer Science, Wroclaw, Poland, July 2007.
• Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type Theory (with Andreas Abel and Thierry Coquand). MPC 2008: 29-56.
• Formal Neighbourhoods, Combinatory Böhm Trees, and Untyped Normalization by Evaluation (with Denis Kuperberg). February 2008. Annals of Pure and Applied Logic 163(2): 122-131.
• Game Semantics and Normalization by Evaluation (with Pierre Clairambault). Foundations of Software Science and Computation Structures 2015: 56-70.

• Normalization by Evaluation for Untyped Combinatory Logic. Talk given at the Stockholm - Uppsala Logic seminar, February 2005.
• Typed and Untyped Normalization by Evaluation. Invited lecture at the Workshop on New Approaches to Software Construction, Tokyo, September 2005.
• Recent News about Normalization by Evaluation for Martin-Löf Type Theory. Proglog-CVS seminar, April 2007.
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe. Talk at Mathematical Foundations of Programming Semantics, New Orleans, LA, USA, April 2007.
• Formal Topology and the Correctness of a Haskell Program for Untyped Normalization by Evaluation Lecture given in Aarhus, 24 October 2007.
• Normalization by Evaluation. Course given at the Midlands Graduate School in the Foundations of Computer Science, Leicester, UK, 30 March - 3 April, 2009.