References

  1. Andreas Abel & Thorsten Altenkirch (2002): A Predicative Analysis of Structural Recursion. Journal of Functional Programming 12(1), pp. 1–41. Available at http://dx.doi.org/10.1017/S0956796801004191.
  2. Andreas Abel & James Chapman (2014): Normalization by Evaluation in the Delay Monad: Literate Agda Code. Available at http://www.cse.chalmers.se/~abela/eptcs14.lagda. 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 http://dx.doi.org/10.1007/978-3-540-70594-9_4.
  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 http://doi.acm.org/10.1145/2500365.2500591.
  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 http://doi.acm.org/10.1145/2429069.2429075.
  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 http://dx.doi.org/10.1016/j.apal.2004.10.003.
  7. Thorsten Altenkirch & James Chapman (2009): Big-step normalisation. Journal of Functional Programming 19(3-4), pp. 311–333. Available at http://dx.doi.org/10.1017/S0956796809007278.
  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 http://www.cse.chalmers.se/~nad/publications/altenkirch-danielsson-par2010.pdf.
  9. Lennart Augustsson (1999): Equality proofs in Cayenne. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.9415. Unpublished note, TeX source see http://www.augustsson.net/Darcs/Cayenne/doc/eqproof.tex.
  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 http://dx.doi.org/10.1109/LICS.1991.151645.
  11. Venanzio Capretta (2005): General Recursion via Coinductive Types. Logical Methods in Computer Science 1(2). Available at http://dx.doi.org/10.2168/LMCS-1(2:1)2005.
  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 http://dx.doi.org/10.1007/3-540-58085-9_72.
  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 http://doi.acm.org/10.1145/2364527.2364546.
  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 http://doi.acm.org/10.1145/237721.237784.
  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 http://doi.acm.org/10.1145/317636.317779.
  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 http://dx.doi.org/10.1007/3-540-60579-7_3.
  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 http://doi.acm.org/10.1145/581478.581501.
  20. INRIA (2012): The Coq Proof Assistant Reference Manual. INRIA, version 8.4 edition. Available at http://coq.inria.fr/.
  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 http://dx.doi.org/10.1145/1863597.1863601.
  22. Grigori Mints (1978): Finite Investigations of Transfinite Derivations. Journal of Soviet Mathematics 10, pp. 548–596. Available at http://dx.doi.org/10.1007/BF01091743. 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: eptcs@eptcs.org
For website issues: webmaster@eptcs.org