skip to main content
10.1145/1292597.1292601acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

A coinductive monad for prop-bounded recursion

Published: 02 October 2007 Publication History

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, and Ulf Norell. Verifying haskell programs using constructive type theory. In Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, pages 62--73, New York, NY, USA, 2005. ACM Press.
[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 and Venanzio Capretta. Nested general recursion and partiality in type theory. Lecture Notes in Computer Science, 2152:121+, 2001.
[4]
Ana Bove. Simple general recursion in type theory. Nordic J. of Computing, 8(1):22--42, 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 and Gerard Huet. The calculus of constructions. Inf. Comput., 76(2-3):95--120, 1988.
[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 and Scott F. Smith. Computational foundations of basic recursive function theory. Theoretical Computer Science, 121(1-2):89--112, 1993.
[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. In TYPES '94: Selected papers from the International Workshop on Types for Proofs and Programs, pages 39--59, London, UK, 1995. Springer-Verlag.
[14]
Eduardo Gimenez. Structural recursive definitions in type theory. In Automata, Languages and Programming, pages 397--408, 1998.
[15]
Herman Geuvers, Erik Poll, and Jan Zwanenburg. Safe proof checking in type theory with y. In CSL, pages 439--452, 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. In TYPES, pages 197--216, 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, 28(3):605--619, 1988.
[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. In Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, pages 74--85, New York, NY, USA, 2005. ACM Press.
[24]
Scott Fraser Smith. Partial objects in type theory. Technical Report TR88-938, 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.

Cited By

View all
  • (2024)Formal Definitions and Proofs for Partial (Co)Recursive FunctionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100999(100999)Online publication date: Jun-2024
  • (2014)Partiality and recursion in interactive theorem provers – an overviewMathematical Structures in Computer Science10.1017/S096012951400011526:1(38-88)Online publication date: 10-Nov-2014
  • (2012)Stop When You Are Almost-FullInteractive Theorem Proving10.1007/978-3-642-32347-8_17(250-265)Online publication date: 2012
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verification
October 2007
76 pages
ISBN:9781595936776
DOI:10.1145/1292597
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 October 2007

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. coinductive types
  2. type theory

Qualifiers

  • Article

Conference

ICFP07
Sponsor:

Acceptance Rates

PLPV '07 Paper Acceptance Rate 6 of 8 submissions, 75%;
Overall Acceptance Rate 18 of 25 submissions, 72%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)10
  • Downloads (Last 6 weeks)1
Reflects downloads up to 14 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Formal Definitions and Proofs for Partial (Co)Recursive FunctionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100999(100999)Online publication date: Jun-2024
  • (2014)Partiality and recursion in interactive theorem provers – an overviewMathematical Structures in Computer Science10.1017/S096012951400011526:1(38-88)Online publication date: 10-Nov-2014
  • (2012)Stop When You Are Almost-FullInteractive Theorem Proving10.1007/978-3-642-32347-8_17(250-265)Online publication date: 2012
  • (2009)Algebra of programming in agdaJournal of Functional Programming10.1017/S095679680900734519:5(545-579)Online publication date: 1-Sep-2009
  • (2008)Fixed point semantics and partial recursion in CoqProceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming10.1145/1389449.1389461(89-96)Online publication date: 15-Jul-2008
  • (2008)A Type of Partial Recursive FunctionsProceedings of the 21st International Conference on Theorem Proving in Higher Order Logics10.1007/978-3-540-71067-7_12(102-117)Online publication date: 18-Aug-2008

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media