A coinductive monad for prop-bounded recursion

ABSTRACT

This paper develops machinery necessary to mechanically import arbitrary functional programs into Coq's type theory, manually strengthen their specifications with additional proofs, and then mechanicaly re-extracting the newly-certified program in a form which is as efficient as the original program. In order to facilitate this goal, the coinductive technique of[Capretta2005] is modified to form a monad whose operators are the constructors of a coinductive type rather than functions defined over the type. The inductive invariant technique of [Krstic2003] is extended to allow optional "after the fact" termination proofs. These proofs inhabit members of Prop, and therefore do not affect extracted code. Compared to [Capretta2005], the new monad makes it possible to directly represent unrestricted recursion without violating productivity requirements [Gimenez1995], and it produces efficient code via Coq's extraction mechanism. The disadvantages of this technique include reliance on the JMeq axiom [McBride2000] and a significantly more complex notion of equality. The resulting technique is packaged as a Coq library, and is suitable for formalizing programs written in any side-effect-free functional language with call-by-value semantics. It can be downloaded from: http://www.cs.berkeley.edu/~megacz/computation.

REFERENCES

• 1: Andreas Abel , Marcin Benke , Ana Bove , John Hughes , Ulf Norell, Verifying haskell programs using constructive type theory, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.62-73, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088355]
• 2: Philippe Audebaud. Partial objects in the calculus of constructions. In Proceedings 6th Annual IEEE Symp. on Logic in Computer Science, LICS'91, Amsterdam, The Netherlands, 15-18 July 1991, pages 86--95. IEEE Computer Society Press, Los Alamitos, CA, 1991.
• 3: Ana Bove , Venanzio Capretta, Nested General Recursion and Partiality in Type Theory, Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, p.121-135, September 03-06, 2001
• 4: Ana Bove, Simple general recursion in type theory, Nordic Journal of Computing, v.8 n.1, p.22-42, Spring 2001
• 5: Venanzio Capretta. General recursion via coinductive types. LMCS-1, 2:1, 2005.
• 6: Venanzio Capretta. Formalization accompanying general recursion via coinductive types (rec coind.v). Downloaded 31-July-2007, 2007.
• 7: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• 8: Development Team For Coq. The Coq Proof Assistant Reference Manual. LogiCal Project, 2006. Version 8.1.
• 9: Robert L. Constable and Scott F. Smith. Partial objects in constructive type theory. In LICS, pages 183--193. IEEE Computer Society, 1987.
• 10: Robert L. Constable , Scott F. Smith, Computational foundations of basic recursive function theory, Theoretical Computer Science, v.121 n.1-2, p.89-112, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90085-8]
• 11: Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log, 65(2):525--549, 2000.
• 12: David Pichardie Gilles Barthe, Julien Forest and Vlad Rusu. Defining and reasoning about recursive functions: a practical tool for the coq proof assistant. In Proc. of 8th International Symposium on Functional and Logic Programming (FLOPS'06), number 3945 in Lecture Notes in Computer Science, pages 114--129. http://www.springer.de/comp/lncs/index.htmlSpringer-Verlag, 2006.
• 13: Eduardo Giménez, Codifying Guarded Definitions with Recursive Schemes, Selected papers from the International Workshop on Types for Proofs and Programs, p.39-59, June 06-10, 1994
• 14: Eduardo Giménez, Structural Recursive Definitions in Type Theory, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.397-408, July 13-17, 1998
• 15: Herman Geuvers , Erik Poll , Jan Zwanenburg, Safe Proof Checking in Type Theory with Y, Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic, p.439-452, September 20-25, 1999
• 16: S. Krstic and J. Matthews. Inductive invariants for nested recursion, 2003.
• 17: D. E. Knuth. Algorithms. 236(4):63--66, 69--72, 79--78, 80, April 1977.
• 18: Conor McBride, Elimination with a Motive, Selected papers from the International Workshop on Types for Proofs and Programs, p.197-216, December 08-12, 2000
• 19: M. Niqui and Y. Bertot. Qarith: Coq formalisation of lazy rational arithmetic, 2003.
• 20: R. S. Nikhil. Id language reference manual (version 90.1). Technical Report 284-2, 1991.
• 21: B. Nordström, Terminating general recursion, BIT, v.28 n.3, p.605-619, 1988 [doi>10.1007/BF01941137]
• 22: Bengt Nordström. The ALF proof editor. In Proceedings of the Workshop on Types for Proofs and Programs, pages 253--266, Nijmegen, 1993.
• 23: Tim Sheard, Putting curry-howard to work, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.74-85, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088356]
• 24: Scott F Smith, Partial Objects in Type Theory, Cornell University, Ithaca, NY, 1988
• 25: Scott F. Smith. Hybrid partial-total type theory. Int. J. Found. Comput. Sci, 6(3):235--263, 1995.
• 26: D. A. Turner. Total functional programming. 10(7):751--768, 2004. http://www.jucs.org/jucs 10 7/totalfunctional programming.
• 27: Philip Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi: Proceedings of the 1992 Marktoberdorf International Summer School. Springer-Verlag, 1993.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory

General Terms:
Verification

Keywords:
coinductive types, type theory