@article(appel:mcallester,
 author       = "Andrew W. Appel and David McAllester",
 year         = "2001",
 title        = "An indexed model of recursive types for foundational proof-carrying code",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "23",
 number       = "5",
 pages        = "657--683",
 doi          = "10.1145/504709.504712",
)
@incollection(barthe:recdef,
 author       = "Gilles Barthe and Julien Forest and David Pichardie and Vlad Rusu",
 year         = "2006",
 title        = "Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant",
 editor       = "Masami Hagiya and Philip Wadler",
 booktitle    = "Functional and Logic Programming",
 series       = "Lecture Notes in Computer Science",
 volume       = "3945",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "114--129",
 doi          = "10.1007/11737414\_9",
)
@inbook(boyer_moore:wos-schrift,
 author       = "Robert S. Boyer and J Strother Moore",
 year         = "1997",
 title        = "Automated reasoning and its applications",
 chapter      = "Mechanized formal reasoning about programs and computing machines",
 pages        = "147--176",
 publisher    = "MIT Press",
 address      = "Cambridge, MA, USA",
 url          = "http://dl.acm.org/citation.cfm?id=271101.271126",
)
@inproceedings(greve:assuming,
 author       = "David Greve",
 year         = "2009",
 title        = "Assuming termination",
 booktitle    = "Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications",
 series       = "ACL2 '09",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "114--122",
 doi          = "10.1145/1637837.1637856",
)
@article(ACL2:theories,
 author       = "Matt Kaufmann and J. Strother Moore",
 year         = "2001",
 title        = "Structured Theory Development for a Mechanized Logic",
 journal      = "J. Autom. Reason.",
 volume       = "26",
 number       = "2",
 pages        = "161--203",
 doi          = "10.1023/A:1026517200045",
)
@article(krauss:phd,
 author       = "Alexander Krauss",
 year         = "2010",
 title        = "Partial and Nested Recursive Function Definitions in Higher-order Logic",
 journal      = "J. Autom. Reason.",
 volume       = "44",
 number       = "4",
 pages        = "303--336",
 doi          = "10.1007/s10817-009-9157-2",
)
@article(manolios_moore:pfun,
 author       = "Panagiotis Manolios and J. Strother Moore",
 year         = "2003",
 title        = "Partial Functions in ACL2",
 journal      = "J. Autom. Reason.",
 volume       = "31",
 number       = "2",
 pages        = "107--127",
 doi          = "10.1023/B:JARS.0000009505.07087.34",
)
@article(moggi:notions,
 author       = "Eugenio Moggi",
 year         = "1991",
 title        = "Notions of computation and monads",
 journal      = "Inf. Comput.",
 volume       = "93",
 number       = "1",
 pages        = "55--92",
 doi          = "10.1016/0890-5401(91)90052-4",
)
@phdthesis(slind:phd,
 author       = "Konrad Slind",
 year         = "1999",
 title        = "Reasoning about Terminating Functional Programs",
 school       = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen",
)