@unknown(abelAltenkirch:jfp02,
 author       = "Andreas Abel and Thorsten Altenkirch",
 year         = "2002",
 title        = "A Predicative Analysis of Structural Recursion",
 journal      = "Journal of Functional Programming",
 volume       = "12",
 number       = "1",
 pages        = "1--41",
 url          = "http://dx.doi.org/10.1017/S0956796801004191",
)
@unknown(abelChapman:msfp14lagda,
 author       = "Andreas Abel and James Chapman",
 year         = "2014",
 title        = "Normalization by Evaluation in the Delay Monad: Literate Agda Code",
 url          = "http://www.cse.chalmers.se/~abela/eptcs14.lagda",
 note         = "Tested with Agda development version and standard library of the date of publication",
)
@unknown(abelCoquandDybjer:mpc08,
 author       = "Andreas Abel and Thierry Coquand and Peter Dybjer",
 year         = "2008",
 title        = "Verifying a Semantic $\beta \eta $-Conversion Test for {Martin-L\"of} Type Theory",
 editor       = "Philippe Audebaud and Christine Paulin-Mohring",
 booktitle    = "Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "5133",
 publisher    = "Springer-Verlag",
 pages        = "29--56",
 url          = "http://dx.doi.org/10.1007/978-3-540-70594-9_4",
)
@unknown(abelPientka:icfp13,
 author       = "Andreas Abel and Brigitte Pientka",
 year         = "2013",
 title        = "Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity",
 editor       = "Greg Morrisett and Tarmo Uustalu",
 booktitle    = "Proceedings of the Eighteenth ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA, September 25-27, 2013",
 publisher    = "ACM Press",
 pages        = "185--196",
 url          = "http://doi.acm.org/10.1145/2500365.2500591",
)
@unknown(abelPientkaThibodeauSetzer:popl13,
 author       = "Andreas Abel and Brigitte Pientka and David Thibodeau and Anton Setzer",
 year         = "2013",
 title        = "Copatterns: Programming Infinite Structures by Observations",
 editor       = "Roberto Giacobazzi and Radhia Cousot",
 booktitle    = "The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'13, Rome, Italy, January 23 - 25, 2013",
 publisher    = "ACM Press",
 pages        = "27--38",
 url          = "http://doi.acm.org/10.1145/2429069.2429075",
)
@unknown(aehligJoachimski:continuousNormalization,
 author       = "Klaus Aehlig and Felix Joachimski",
 year         = "2005",
 title        = "Continuous Normalization for the Lambda-Calculus and {G}\"odel's {T}",
 journal      = "Annals of Pure and Applied Logic",
 volume       = "133",
 pages        = "39--71",
 url          = "http://dx.doi.org/10.1016/j.apal.2004.10.003",
)
@unknown(altenkirchChapman:bigStepNormalisation,
 author       = "Thorsten Altenkirch and James Chapman",
 year         = "2009",
 title        = "Big-step normalisation",
 journal      = "Journal of Functional Programming",
 volume       = "19",
 number       = "3-4",
 pages        = "311--333",
 url          = "http://dx.doi.org/10.1017/S0956796809007278",
)
@unknown(altenkirchDanielsson:par10,
 author       = "Thorsten Altenkirch and Nils Anders Danielsson",
 year         = "2010",
 title        = "Termination Checking in the Presence of Nested Inductive and Coinductive Types",
 howpublished = "Short note supporting a talk given at PAR 2010, Workshop on Partiality and Recursion in Interactive Theorem Provers, FLoC 2010",
 url          = "http://www.cse.chalmers.se/~nad/publications/altenkirch-danielsson-par2010.pdf",
)
@unknown(augustsson:equalityProofs,
 author       = "Lennart Augustsson",
 year         = "1999",
 title        = "Equality proofs in {Cayenne}",
 url          = "http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.9415",
 note         = "Unpublished note, TeX source see http://www.augustsson.net/Darcs/Cayenne/doc/eqproof.tex",
)
@unknown(bergerSchwichtenberg:lics91,
 author       = "Ulrich Berger and Helmut Schwichtenberg",
 year         = "1991",
 title        = "An Inverse to the Evaluation Functional for Typed $\lambda $-calculus",
 booktitle    = "Sixth Annual Symposium on Logic in Computer Science (LICS '91), July, 1991, Amsterdam, The Netherlands, Proceedings",
 publisher    = "IEEE Computer Society Press",
 pages        = "203--211",
 url          = "http://dx.doi.org/10.1109/LICS.1991.151645",
)
@unknown(capretta:generalRecursionViaCoinductiveTypes,
 author       = "Venanzio Capretta",
 year         = "2005",
 title        = "General Recursion via Coinductive Types",
 journal      = "Logical Methods in Computer Science",
 volume       = "1",
 number       = "2",
 url          = "http://dx.doi.org/10.2168/LMCS-1(2:1)2005",
)
@unknown(chapman:PhD,
 author       = "James Chapman",
 year         = "2009",
 title        = "Type Checking and Normalization",
 type         = "Ph.D. thesis",
 school       = "School of Computer Science, University of Nottingham",
)
@unknown(coquand:infiniteobjects,
 author       = "Thierry Coquand",
 year         = "1993",
 title        = "Infinite Objects in Type Theory",
 editor       = "H. Barendregt and T. Nipkow",
 booktitle    = "Types for Proofs and Programs (TYPES '93)",
 series       = "Lecture Notes in Computer Science",
 volume       = "806",
 publisher    = "Springer-Verlag",
 pages        = "62--78",
 url          = "http://dx.doi.org/10.1007/3-540-58085-9_72",
)
@unknown(danielsson:icfp12,
 author       = "Nils Anders Danielsson",
 year         = "2012",
 title        = "Operational semantics using the partiality monad",
 editor       = "Peter Thiemann and Robby Bruce Findler",
 booktitle    = "Proceedings of the Seventeenth ACM SIGPLAN International Conference on Functional Programming, ICFP'12, Copenhagen, Denmark, September 9-15, 2012",
 publisher    = "ACM Press",
 pages        = "127--138",
 url          = "http://doi.acm.org/10.1145/2364527.2364546",
)
@unknown(danvy:tdpe,
 author       = "Olivier Danvy",
 year         = "1999",
 title        = "Type-Directed Partial Evaluation",
 editor       = "John Hatcliff and Torben {\AE }. Mogensen and Peter Thiemann",
 booktitle    = "Partial Evaluation -- Practice and Theory, DIKU 1998 International Summer School, Copenhagen, Denmark, June 29 - July 10, 1998",
 series       = "Lecture Notes in Computer Science",
 volume       = "1706",
 publisher    = "Springer-Verlag",
 pages        = "367--411",
 url          = "http://doi.acm.org/10.1145/237721.237784",
)
@unknown(escardo:metricPCF,
 author       = "Martin H. Escardo",
 year         = "1999",
 title        = "A metric model of {PCF}",
 howpublished = "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)",
)
@unknown(ganzFriedmanWand:icfp99,
 author       = "Steven E. Ganz and Daniel P. Friedman and Mitchell Wand",
 year         = "1999",
 title        = "Trampolined Style",
 editor       = "Didier R{\'e}mi and Peter Lee",
 booktitle    = "Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP '99), Paris, France",
 publisher    = "ACM Press",
 pages        = "18--27",
 url          = "http://doi.acm.org/10.1145/317636.317779",
)
@unknown(gimenez:guardeddefinitions,
 author       = "Eduardo Gim\'enez",
 year         = "1995",
 title        = "Codifying Guarded Definitions with Recursive Schemes",
 editor       = "Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith",
 booktitle    = "Types for Proofs and Programs, International Workshop TYPES'94, B{\r a}stad, Sweden, June 6-10, 1994, Selected Papers",
 series       = "Lecture Notes in Computer Science",
 volume       = "996",
 publisher    = "Springer-Verlag",
 pages        = "39--59",
 url          = "http://dx.doi.org/10.1007/3-540-60579-7_3",
)
@unknown(gregoireLeroy:icfp02,
 author       = "Benjamin Gr{\'e}goire and Xavier Leroy",
 year         = "2002",
 title        = "A compiled implementation of strong reduction",
 booktitle    = "Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002",
 series       = "SIGPLAN Notices",
 volume       = "37",
 publisher    = "ACM Press",
 pages        = "235--246",
 url          = "http://doi.acm.org/10.1145/581478.581501",
)
@unknown(inria:coq84,
 author       = "INRIA",
 year         = "2012",
 title        = "The {Coq} Proof Assistant Reference Manual",
 organization = "INRIA",
 edition      = "version 8.4",
 url          = "http://coq.inria.fr/",
)
@unknown(kellerAltenkirch:msfp10,
 author       = "Chantal Keller and Thorsten Altenkirch",
 year         = "2010",
 title        = "{Hereditary Substitutions for Simple Types, Formalized}",
 editor       = "V. Capretta and J. Chapman",
 booktitle    = "Third Workshop on Mathematically Structured Functional Programming, MSFP 2010, Baltimore, USA, September 25, 2010",
 publisher    = "ACM Press",
 address      = "Baltimore, USA",
 url          = "http://dx.doi.org/10.1145/1863597.1863601",
)
@unknown(mints:contNorm,
 author       = "Grigori Mints",
 year         = "1978",
 title        = "Finite Investigations of Transfinite Derivations",
 journal      = "Journal of Soviet Mathematics",
 volume       = "10",
 pages        = "548--596",
 url          = "http://dx.doi.org/10.1007/BF01091743",
 note         = "Translated from: Zap. Nauchn. Semin. LOMI 49 (1975).",
)
@unknown(prawitz:natDed,
 author       = "Dag Prawitz",
 year         = "1965",
 title        = "Natural Deduction",
 publisher    = "Almqvist \& Wiksell, Stockholm",
 note         = "Republication by Dover Publications Inc., Mineola, New York, 2006",
)
@unknown(watkins:concurrentLFTR,
 author       = "Kevin Watkins and Iliano Cervesato and Frank Pfenning and David Walker",
 year         = "2003",
 title        = "A concurrent logical framework {I}: Judgements and properties",
 type         = "Technical Report",
 institution  = "School of Computer Science, Carnegie Mellon University, Pittsburgh",
)