Skip to main content
SpringerLink
Log in

Typing Total Recursive Functions in Coq

  • Conference paper
Interactive Theorem Proving (ITP 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10499))

Included in the following conference series:

Abstract

We present a (relatively) short mechanized proof that Coq types any recursive function which is provably total in Coq. The well-founded (and terminating) induction scheme, which is the foundation of Coq recursion, is maximal. We implement an unbounded minimization scheme for decidable predicates. It can also be used to reify a whole category of undecidable predicates. This development is purely constructive and requires no axiom. Hence it can be integrated into any project that might assume additional axioms.

Work partially supported by the TICAMORE project (ANR grant 16-CE91-0002).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    From which the term \(t_f \,{\mathtt {:=}}\,\varvec{v}\,{\mapsto }\,{\mathtt {proj1\_sig}}(Q\;\varvec{v})\) of (CiT) is trivially derived.

  2. 2.

    It is difficult to use a word more accurate than “seems” because the relevant discussion in [2] is just a short outline of an approach, not a proof or an actual implementation.

  3. 3.

    Of course this statement is of philosophical nature. We do not claim that assuming additional axiom is evil, but carelessly adding axioms is a recipe for inconsistencies.

References

  1. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)

    Book  Google Scholar 

  2. Bove, A., Capretta, V.: Modelling general recursion in type theory. Math. Struct. Comput. Sci. 15(4), 671–708 (2005)

    Article  MathSciNet  Google Scholar 

  3. Castéran, P.: Utilisation en Coq de l’opérateur de description (2007). http://jfla.inria.fr/2007/actes/PDF/03_casteran.pdf

  4. Coen, C.S., Valentini, S.: General recursion and formal topology. In: Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, EPiC Series, Edinburgh, UK, 15 July 2010, vol. 5, pp. 71–82. EasyChair (2010)

    Google Scholar 

  5. Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)

    MATH  Google Scholar 

  6. Krivine, J.: Lambda-Calculus, Types and Models. Ellis Horwood Series in Computers and Their Applications. Ellis Horwood, Masson (1993)

    MATH  Google Scholar 

  7. Larchey-Wendling, D.: A constructive mechanization of Lambda Calculus in Coq (2017). http://www.loria.fr/~larchey/Lambda_Calculus

  8. Norrish, M.: Mechanised computability theory. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 297–311. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22863-6_22

    Chapter  Google Scholar 

  9. Soare, R.I.: Recursively Enumerable Sets and Degrees. Springer-Verlag New York Inc., New York (1987)

    Book  Google Scholar 

  10. Werner, B.: Sets in types, types in sets. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530–546. Springer, Heidelberg (1997). doi:10.1007/BFb0014566

    Chapter  Google Scholar 

  11. Xu, J., Zhang, X., Urban, C.: Mechanising turing machines and computability theory in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147–162. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39634-2_13

    Chapter  Google Scholar 

  12. Zammit, V.: A mechanisation of computability theory in HOL. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 431–446. Springer, Heidelberg (1996). doi:10.1007/BFb0105420

    Chapter  Google Scholar 

  13. Zammit, V.: A proof of the S-m-n theorem in Coq. Technical report, The Computing Laboratory, The University of Kent, Canterbury, Kent, UK, March 1997. http://kar.kent.ac.uk/21524/

Download references

Author information

Authors and Affiliations

  1. LORIA – CNRS, Nancy, France

    Dominique Larchey-Wendling

Authors
  1. Dominique Larchey-Wendling
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dominique Larchey-Wendling .

Editor information

Editors and Affiliations

  1. University of Brasília, Brasília D.F., Brazil

    Mauricio Ayala-Rincón

  2. NASA, Hampton, VA, USA

    César A. Muñoz

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Larchey-Wendling, D. (2017). Typing Total Recursive Functions in Coq. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66107-0_24

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66106-3

  • Online ISBN: 978-3-319-66107-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation