References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. Eugenio Moggi (1991): Notions of computation and monads. Inf. Comput. 93(1), pp. 55–92, doi:10.1016/0890-5401(91)90052-4.
  9. Konrad Slind (1999): Reasoning about Terminating Functional Programs. Institut für Informatik, Technische Universität München.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org