1. Andreas Abel & Thorsten Altenkirch (2002): A Predicative Analysis of Structural Recursion. Journal of Functional Programming 12(1), pp. 1–41. Available at
  2. Andreas Abel & James Chapman (2014): Normalization by Evaluation in the Delay Monad: Literate Agda Code. Available at Tested with Agda development version and standard library of the date of publication.
  3. Andreas Abel, Thierry Coquand & Peter Dybjer (2008): Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory. In: Philippe Audebaud & Christine Paulin-Mohring: Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, Lecture Notes in Computer Science 5133. Springer-Verlag, pp. 29–56. Available at
  4. Andreas Abel & Brigitte Pientka (2013): Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity. In: Greg Morrisett & Tarmo Uustalu: Proceedings of the Eighteenth ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA, September 25-27, 2013. ACM Press, pp. 185–196. Available at
  5. Andreas Abel, Brigitte Pientka, David Thibodeau & Anton Setzer (2013): Copatterns: Programming Infinite Structures by Observations. In: Roberto Giacobazzi & Radhia Cousot: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'13, Rome, Italy, January 23 - 25, 2013. ACM Press, pp. 27–38. Available at
  6. Klaus Aehlig & Felix Joachimski (2005): Continuous Normalization for the Lambda-Calculus and Gödel's T. Annals of Pure and Applied Logic 133, pp. 39–71. Available at
  7. Thorsten Altenkirch & James Chapman (2009): Big-step normalisation. Journal of Functional Programming 19(3-4), pp. 311–333. Available at
  8. Thorsten Altenkirch & Nils Anders Danielsson (2010): Termination Checking in the Presence of Nested Inductive and Coinductive Types. Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010. Available at
  9. Lennart Augustsson (1999): Equality proofs in Cayenne. Available at Unpublished note, TeX source see
  10. Ulrich Berger & Helmut Schwichtenberg (1991): An Inverse to the Evaluation Functional for Typed λ-calculus. In: Sixth Annual Symposium on Logic in Computer Science (LICS '91), July, 1991, Amsterdam, The Netherlands, Proceedings. IEEE Computer Society Press, pp. 203–211. Available at
  11. Venanzio Capretta (2005): General Recursion via Coinductive Types. Logical Methods in Computer Science 1(2). Available at
  12. James Chapman (2009): Type Checking and Normalization. Ph.D. thesis. School of Computer Science, University of Nottingham.
  13. Thierry Coquand (1993): Infinite Objects in Type Theory. In: H. Barendregt & T. Nipkow: Types for Proofs and Programs (TYPES '93), Lecture Notes in Computer Science 806. Springer-Verlag, pp. 62–78. Available at
  14. Nils Anders Danielsson (2012): Operational semantics using the partiality monad. In: Peter Thiemann & Robby Bruce Findler: Proceedings of the Seventeenth ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012. ACM Press, pp. 127–138. Available at
  15. Olivier Danvy (1999): Type-Directed Partial Evaluation. In: John Hatcliff, Torben Æ. Mogensen & Peter Thiemann: Partial Evaluation – Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998, Lecture Notes in Computer Science 1706. Springer-Verlag, pp. 367–411. Available at
  16. Martin H. Escardo (1999): A metric model of PCF. Presented at the Workshop on Realizability Semantics and Applications, June 30-July 1, 1999 (associated to the Federated Logic Conference, held in Trento, June 29-July 12, 1999).
  17. Steven E. Ganz, Daniel P. Friedman & Mitchell Wand (1999): Trampolined Style. In: Didier Rémi & Peter Lee: Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), Paris, France. ACM Press, pp. 18–27. Available at
  18. Eduardo Giménez (1995): Codifying Guarded Definitions with Recursive Schemes. In: Peter Dybjer, Bengt Nordström & Jan Smith: Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, Lecture Notes in Computer Science 996. Springer-Verlag, pp. 39–59. Available at
  19. Benjamin Grégoire & Xavier Leroy (2002): A compiled implementation of strong reduction. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, SIGPLAN Notices 37. ACM Press, pp. 235–246. Available at
  20. INRIA (2012): The Coq Proof Assistant Reference Manual. INRIA, version 8.4 edition. Available at
  21. Chantal Keller & Thorsten Altenkirch (2010): Hereditary Substitutions for Simple Types, Formalized. In: V. Capretta & J. Chapman: Third Workshop on Mathematically Structured Functional Programming, MSFP 2010, Baltimore, USA, September 25, 2010. ACM Press, Baltimore, USA. Available at
  22. Grigori Mints (1978): Finite Investigations of Transfinite Derivations. Journal of Soviet Mathematics 10, pp. 548–596. Available at Translated from: Zap. Nauchn. Semin. LOMI 49 (1975)..
  23. Dag Prawitz (1965): Natural Deduction. Almqvist & Wiksell, Stockholm. Republication by Dover Publications Inc., Mineola, New York, 2006.
  24. Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2003): A concurrent logical framework I: Judgements and properties. Technical Report. School of Computer Science, Carnegie Mellon University, Pittsburgh.

Comments and questions to:
For website issues: