nach oben

Erschienen in:

2017 | Supplement | Buchkapitel

Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic

verfasst von : Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondřej Kunčar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel

Erschienen in: Frontiers of Combining Systems

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We describe a line of work that started in 2011 towards enriching Isabelle/HOL’s language with coinductive datatypes, which allow infinite values, and with a more expressive notion of inductive datatype than previously supported by any system based on higher-order logic. These (co)datatypes are complemented by definitional principles for (co)recursive functions and reasoning principles for (co)induction. In contrast with other systems offering codatatypes, no additional axioms or logic extensions are necessary with our approach.

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

Nächstes Kapitel Designing Theory Solvers with Extensions

Bartels, F.: Generalised coinduction. Math. Struct. Comput. Sci. 13(2), 321–348 (2003)MathSciNetCrossRefMATH

Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: Formalization of Knuth–Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs (2016). Formal proof development. http://isa-afp.org/entries/Lambda_Free_KBOs.shtml

Becker, H., Blanchette, J.C., Waldmann, U., Wand, D.: A transfinite Knuth–Bendix order for lambda-free higher-order terms. In: de Moura, L. (ed.) CADE-26. LNCS, vol. 10395, pp. 432–453. Springer, Cham (2017). doi:10.1007/978-3-319-63046-5_27 CrossRef

Berghofer, S., Wenzel, M.: Inductive datatypes in HOL—lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 19–36. Springer, Heidelberg (1999). doi:10.1007/3-540-48256-3_3 CrossRef

Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development–Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004). doi:10.1007/978-3-662-07964-5 CrossRefMATH

Blanchette, J.C.: Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions. Softw. Qual. J. 21(1), 101–126 (2013)CrossRef

Blanchette, J.C., Fleury, M., Traytel, D.: Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. In: Miller, D. (ed.) FSCD 2017. LIPIcs, vol. 84, pp. 11:1–11:17 (2017). Schloss Dagstuhl—Leibniz-Zentrum für Informatik

Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_11 CrossRef

Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149–179 (2017)MathSciNetCrossRefMATH

10.

Blanchette, J.C., Bouzy, A., Lochbihler, A., Popescu, A., Traytel, D.: Friends with benefits. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 111–140. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54434-1_5 CrossRef

11.

Blanchette, J.C., Fleury, M., Traytel, D.: Formalization of nested multisets, hereditary multisets, and syntactic ordinals. Archive of Formal Proofs (2016). Formal proof development. http://isa-afp.org/entries/Nested_Multisets_Ordinals.shtml

12.

Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_7

13.

Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: Ouaknine, J. (ed.) LICS 2017. IEEE Computer Society (2017)

14.

Blanchette, J.C., Popescu, A., Traytel, D.: Abstract completeness. Archive of Formal Proofs (2014). Formal proof development. http://isa-afp.org/entries/Abstract_Completeness.shtml

15.

Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 111–127. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_8

16.

Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 46–60. Springer, Cham (2014). doi:10.1007/978-3-319-08587-6_4

17.

Blanchette, J.C., Popescu, A., Traytel, D.: Foundational extensible corecursion–a proof assistant perspective. In: Fisher, K., Reppy, J.H. (eds.) ICFP 2015, pp. 192–204. ACM (2015)

18.

Blanchette, J.C., Popescu, A., Traytel, D.: Witnessing (co)datatypes. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 359–382. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46669-8_15 CrossRef

19.

Bulwahn, L., Krauss, A., Nipkow, T.: Finding lexicographic orders for termination proofs in Isabelle/HOL. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 38–53. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74591-4_5 CrossRef

20.

Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. In: Maurer, H.A. (ed.) ICALP 1979. LNCS, vol. 71, pp. 188–202. Springer, Heidelberg (1979). doi:10.1007/3-540-09510-1_15 CrossRef

21.

Gödel, K.: Über die Vollständigkeit des Logikkalküls. Ph.D. thesis, Universität Wien (1929)

22.

Gunter, E.L.: Why we can’t have SML-style datatype declarations in HOL. In: TPHOLs 1992. IFIP Transactions, vol. A-20, pp. 561–568. North-Holland/Elsevier (1993)

23.

Hinze, R., Paterson, R.: Finger trees: a simple general-purpose data structure. J. Funct. Program. 16(2), 197–217 (2006)MathSciNetCrossRefMATH

24.

Hölzl, J.: Markov chains and Markov decision processes in Isabelle/HOL. J. Autom. Reason. doi:10.1007/s10817-016-9401-5

25.

Hölzl, J.: Markov processes in Isabelle/HOL. In: Bertot, Y., Vafeiadis, V. (eds.) CPP 2017, pp. 100–111. ACM (2017)

26.

Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Cham (2013). doi:10.1007/978-3-319-03545-1_9 CrossRef

27.

Kleene, S.C.: Mathematical Logic. Wiley, New York (1967)MATH

28.

Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, pp. 260–270. ACM (2017)

29.

Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 589–603. Springer, Heidelberg (2006). doi:10.1007/11814771_48 CrossRef

30.

Lochbihler, A.: Jinja with threads. Archive of Formal Proofs (2007). Formal proof development. http://isa-afp.org/entries/JinjaThreads.shtml

31.

Lochbihler, A.: Coinductive. Archive of Formal Proofs (2010). Formal proof development. http://afp.sf.net/entries/Coinductive.shtml

32.

Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427–447. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11957-6_23 CrossRef

33.

Lochbihler, A.: Making the Java memory model safe. ACM Trans. Program. Lang. Syst. 35(4), 12:1–12:65 (2014)

34.

Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503–531. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49498-1_20 CrossRef

35.

Lochbihler, A., Hölzl, J.: Recursive functions on lazy lists via domains and topologies. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 341–357. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_22

36.

Meier, F.: Non-uniform datatypes in Isabelle/HOL. M.Sc. thesis, ETH Zürich (2016)

37.

Milius, S., Moss, L.S., Schwencke, D.: Abstract GSOS rules and a modular treatment of recursive definitions. Log. Methods Comput. Sci. 9(3), 1–52 (2013)

38.

Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24 CrossRef

39.

Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). doi:10.1007/3-540-45949-9 MATH

40.

Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1999)MATH

41.

Panny, L.: Primitively (co)recursive function definitions for Isabelle/HOL. B.Sc. thesis, Technische Universität München (2014)

42.

Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reason. 58(3), 341–362 (2017)MathSciNetCrossRefMATH

43.

Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP 1983, pp. 513–523 (1983)

44.

Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 194–218. Springer, Heidelberg (1998). doi:10.1007/BFb0055624 CrossRef

45.

Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 114–130. Springer, Cham (2013). doi:10.1007/978-3-319-03545-1_8 CrossRef

46.

Sternagel, C., Thiemann, R.: Deriving comparators and show functions in Isabelle/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 421–437. Springer, Cham (2015). doi:10.1007/978-3-319-22102-1_28

47.

Sternagel, C., Thiemann, R.: Deriving class instances for datatypes. Archive of Formal Proofs (2015). Formal proof development. http://isa-afp.org/entries/Deriving.shtml

48.

Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452–468. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_31 CrossRef

49.

Torlak, E., Jackson, D.: Kodkod: a relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_49 CrossRef

50.

Traytel, D.: Formal languages, formally and coinductively. In: Kesner, D., Pientka, B. (eds.) FSCD 2016. LIPIcs, vol. 52, pp. 31:1–31:17 (2016). Schloss Dagstuhl—Leibniz-Zentrum für Informatik

51.

Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic—category theory applied to theorem proving. In: LICS 2012, pp. 596–605. IEEE Computer Society (2012)

52.

Traytel, D.: A category theory based (co)datatype package for Isabelle/HOL. M.Sc. thesis, Technische Universität München (2012)

53.

Wenzel, M.: Isabelle/Isar—a generic framework for human-readable proof documents. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric 10(23), 277–298 (2007). Uniwersytet w Białymstoku

54.

Wenzel, M.: Re: [isabelle] “Unfolding” the sum-of-products encoding of datatypes (2015). https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-November/msg00082.html

Titel: Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic
verfasst von: Julian Biendarra
Jasmin Christian Blanchette
Aymeric Bouzy
Martin Desharnais
Mathias Fleury
Johannes Hölzl
Ondřej Kunčar
Andreas Lochbihler
Fabian Meier
Lorenz Panny
Andrei Popescu
Christian Sternagel
René Thiemann
Dmitriy Traytel
Verlag: Springer International Publishing
Buch: Frontiers of Combining Systems
Print ISBN: 978-3-319-66166-7

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

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-66167-4_1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"