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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
James Chapman (2009):
Type Checking and Normalization.
Ph.D. thesis.
School of Computer Science, University of Nottingham.
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.
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.
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.
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).
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.
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.
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.
INRIA (2012):
The Coq Proof Assistant Reference Manual.
INRIA,
version 8.4 edition.
Available at http://coq.inria.fr/.
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.
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)..
Dag Prawitz (1965):
Natural Deduction.
Almqvist & Wiksell, Stockholm.
Republication by Dover Publications Inc., Mineola, New York, 2006.
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.