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