Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
An Isabelle/HOL Formalisation of Green’s Theorem Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Modular Dependent Induction in Coq, Mendler-Style

verfasst von : Paolo Torrini

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Algebraic Numbers in Isabelle/HOL
Nächstes Kapitel Formalized Timed Automata
Literatur
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.
Metadaten
Titel
Modular Dependent Induction in Coq, Mendler-Style
verfasst von
Paolo Torrini
Copyright-Jahr
2016
Buch
Interactive Theorem Proving

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

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

Copyright-Jahr: 2016

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

Premium Partner

    Bildnachweise