Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
An Isabelle/HOL Formalisation of Green’s Theorem Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Modular Dependent Induction in Coq, Mendler-Style

Author : Paolo Torrini

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Algebraic Numbers in Isabelle/HOL
next chapter Formalized Timed Automata
Literature
1.
Abbott, M., Altenkirch, T., Ghani, N.: Containers constructing strictly positive types. Theoret. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRefMATH
2.
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)MathSciNetCrossRefMATH
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)
5.
Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development – Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)CrossRefMATH
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)CrossRef
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)
8.
9.
Delaware, B., Keuchel, S., Schrijvers, T., Oliveira, B.C.d.S.: Modular monadic meta-theory. In: ICFP 2013, pp. 319–330. ACM (2013)
10.
11.
Delaware, B., Oliveira, B.C.d.S., Schrijvers, T.: Meta-theory à la carte. In: Proceedings of POPL 2013, pp. 207–218 (2013)
12.
Geuvers, H.: Inductive and coinductive types with iteration and recursion. In: Types for Proofs and Programs, pp. 193–217 (1992)
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)CrossRef
14.
15.
Keuchel, S., Schrijvers, T.: Generic datatypes à la carte. In: 9th ACM SIGPLAN Workshop on Generic Programming (WGP), pp. 1–11 (2013)
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)CrossRef
17.
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)MathSciNetCrossRefMATH
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)CrossRef
20.
21.
22.
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)
24.
Uustalu, T., Vene, V.: Mendler-style inductive types, categorically. Nord. J. Comput. 6(3), 343 (1999)MathSciNetMATH
25.
Uustalu, T., Vene, V.: Coding recursion a la Mendler (extended abstract). Technical report, Department of Computer Science, Utrecht University (2000)
26.
27.
Metadata
Title
Modular Dependent Induction in Coq, Mendler-Style
Author
Paolo Torrini
Copyright Year
2016
Book
Interactive Theorem Proving

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

Electronic ISBN: 978-3-319-43144-4

Copyright Year: 2016

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

Premium Partner

    Image Credits