Skip to main content
SpringerLink
Log in

Modular Dependent Induction in Coq, Mendler-Style

  • Conference paper
  • First Online:
Interactive Theorem Proving (ITP 2016)

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

Included in the following conference series:

Abstract

Modular datatypes can be given a direct encoding in Coq using Church-style encodings, but this makes inductive reasoning generally problematic. We show how Mendler-style induction can be used to supplement existing techniques in modular inductive reasoning, and we present a novel technique to apply Mendler-style induction in presence of dependent induction. This results in type-based, conventional-looking proofs that take better advantage of existing Coq tactics and depend less pervasively on general semantic conditions, reducing the need for boilerplate.

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

References

  1. Abbott, M., Altenkirch, T., Ghani, N.: Containers constructing strictly positive types. Theoret. Comput. Sci. 342(1), 3–27 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  2. Abel, A.: Type-based termination of generic programs. Sci. Comput. Program. 74(8), 550–567 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  3. Abel, A., Matthes, R., Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theoret. Comput. Sci. 333(1–2), 3–66 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  4. Ahn, K.Y., Sheard, T.: A hierarchy of Mendler style recursion combinators: taming inductive datatypes with negative occurrences. In: Proceedings of ICFP 2011, pp. 234–246. ACM (2011)

    Google Scholar 

  5. Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    Book  MATH  Google Scholar 

  6. Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda – A functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73–78. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Churchill, M., Mosses, P.D., Sculthorpe, N., Torrini, P.: Reusable components of semantic specifications. In: Chiba, S., Tanter, É., Ernst, E., Hirschfeld, R. (eds.) Transactions on AOSD XII. LNCS, vol. 8989, pp. 132–179. Springer, Heidelberg (2015)

    Google Scholar 

  8. Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76, 95–120 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  9. Delaware, B., Keuchel, S., Schrijvers, T., Oliveira, B.C.d.S.: Modular monadic meta-theory. In: ICFP 2013, pp. 319–330. ACM (2013)

    Google Scholar 

  10. Delaware, B., Keuchel, S., Schrijvers, T., Oliveira, B.C.d.S.: MTC/3MT-Coq development (2013). http://people.csail.mit.edu/bendy/3MT/

  11. Delaware, B., Oliveira, B.C.d.S., Schrijvers, T.: Meta-theory à la carte. In: Proceedings of POPL 2013, pp. 207–218 (2013)

    Google Scholar 

  12. Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Types for Proofs and Programs, pp. 193–217 (1992)

    Google Scholar 

  13. Hagino, T.: A typed lambda calculus with categorical type constructors. In: Pitt, D.H., Poignê, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 283, pp. 140–157. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  14. Hutton, G.: A tutorial on the universality and expressiveness of fold. J. Funct. Program. 9(4), 355–372 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  15. Keuchel, S., Schrijvers, T.: Generic datatypes à la carte. In: 9th ACM SIGPLAN Workshop on Generic Programming (WGP), pp. 1–11 (2013)

    Google Scholar 

  16. Keuchel, S., Weirich, S., Schrijvers, T.: Needle and Knot: binder boilerplate tied up. In: Thiemann, P. (ed.) ESOP 2016. LNCS, pp. 419–445. Springer, Heidelberg (2016)

    Chapter  Google Scholar 

  17. Matthes, R.: Map fusion for nested datatypes in intensional type theory. Sci. Comput. Program. 76(3), 204–224 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  18. Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Logic 51(1–2), 159–172 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  19. Pfenning, F., Paulin-Mohring, C.: Inductively Defined types in the calculus of constructions. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) Mathematical Foundations of Programming Semantic. LNCS, vol. 442, pp. 209–228. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  20. Swierstra, W.: Data types à la carte. J. Funct. Program. 18(4), 423–436 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  21. Torrini, P.: Language specification and type preservation proofs in Coq-companion code (2015). http://cs.swan.ac.uk/cspt/MDTC

  22. Torrini, P.: Modular induction in Coq – companion code (2016). https://bitbucket.org/ptorrx/modind

  23. Torrini, P., Schrijvers, T.: Reasoning about modular datatypes with Mendler induction. In: Matthes, R., Mio, M. (eds.) Proceedings of FICS 2015. EPTCS, pp. 143–157 (2015)

    Google Scholar 

  24. Uustalu, T., Vene, V.: Mendler-style inductive types, categorically. Nord. J. Comput. 6(3), 343 (1999)

    MathSciNet  MATH  Google Scholar 

  25. Uustalu, T., Vene, V.: Coding recursion a la Mendler (extended abstract). Technical report, Department of Computer Science, Utrecht University (2000)

    Google Scholar 

  26. Wadler, P.: Recursive types for free! (1990). http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt

  27. Wadler, P.: The expression problem (1998). http://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt

Download references

Acknowledgments

We thank Fredrik Nordvall Forsberg, Tom Schrijvers, Steven Keuchel and the anonymous reviewers for important feedback and discussion. This research was supported by EU funding (Horizon 2020, grant 640954) to KU Leuven for the GRACeFUL project

Author information

Authors and Affiliations

  1. Department of Computer Science, KU Leuven, Leuven, Belgium

    Paolo Torrini

Authors
  1. Paolo Torrini
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Paolo Torrini .

Editor information

Editors and Affiliations

  1. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Jasmin Christian Blanchette

  2. Inria Nancy – Grand Est, Villers-lès-Nancy, France

    Stephan Merz

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Torrini, P. (2016). Modular Dependent Induction in Coq, Mendler-Style. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-43144-4_25

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-43143-7

  • Online ISBN: 978-3-319-43144-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation