Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Book cover Frontiers of Combining Systems (FroCoS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10483))

Included in the following conference series:

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.

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 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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. Bartels, F.: Generalised coinduction. Math. Struct. Comput. Sci. 13(2), 321–348 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  2. 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

  3. 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

    Chapter  Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. 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

    Book  MATH  Google Scholar 

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

    Article  Google Scholar 

  7. 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

    Google Scholar 

  8. 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

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

  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

    Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

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

    Google Scholar 

  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)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

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

    MATH  Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

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

    Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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  Google Scholar 

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

    MATH  Google Scholar 

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

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Google Scholar 

  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)

    Google Scholar 

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

    Google Scholar 

  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

    Google Scholar 

  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

Download references

Acknowledgments

We first want to acknowledge the support and encouragement of past and current bosses: David Basin, Wan Fokkink, Stephan Merz, Aart Middeldorp, Tobias Nipkow, and Christoph Weidenbach. We are grateful to the FroCoS 2017 program chairs, Clare Dixon and Marcelo Finger, and to the program committee for giving us this opportunity to present our research. We are also indebted to Andreas Abel, Stefan Berghofer, Sascha Böhme, Lukas Bulwahn, Elsa Gunter, Florian Haftmann, Martin Hofmann, Brian Huffman, Lars Hupel, Alexander Krauss, Peter Lammich, Rustan Leino, Stefan Milius, Lutz Schröder, Mark Summerfield, Christian Urban, Daniel Wand, and Makarius Wenzel, and to dozens of anonymous reviewers (including those who rejected our manuscript “Witnessing (co)datatypes” [18] six times).

Blanchette was supported by the Deutsche Forschungsgemeinschaft (DFG) projects “Quis Custodiet” (NI 491/11-2) and “Den Hammer härten” (NI 491/14-1). He also received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Hölzl was supported by the DFG project “Verifikation probabilistischer Modelle in interaktiven Theorembeweisern” (NI 491/15-1). Kunčar and Popescu were supported by the DFG project “Security Type Systems and Deduction” (NI 491/13-2 and NI 491/13-3) as part of the program Reliably Secure Software Systems (RS\(^3\), priority program 1496). Kunčar was also supported by the DFG project “Integration der Logik HOL mit den Programmiersprachen ML und Haskell” (NI 491/10-2). Lochbihler was supported by the Swiss National Science Foundation (SNSF) grant “Formalising Computational Soundness for Protocol Implementations” (153217). Popescu was supported by the UK Engineering and Physical Sciences Research Council (EPSRC) starting grant “VOWS: Verification of Web-based Systems” (EP/N019547/1). Sternagel and Thiemann were supported by the Austrian Science Fund (FWF): P27502 and Y757. Traytel was supported by the DFG program “Programm- und Modell-Analyse” (PUMA, doctorate program 1480). The authors are listed alphabetically.

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität München, Munich, Germany

    Julian Biendarra & Ondřej Kunčar

  2. Vrije Universiteit Amsterdam, Amsterdam, The Netherlands

    Jasmin Christian Blanchette

  3. Max-Planck-Institut für Informatik, Saarland Informatics Campus, Saarbrücken, Germany

    Jasmin Christian Blanchette & Mathias Fleury

  4. InstantJob, Paris, France

    Aymeric Bouzy

  5. Ludwig-Maximilians-Universität München, Munich, Germany

    Martin Desharnais

  6. Carnegie Mellon University, Pittsburgh, USA

    Johannes Hölzl

  7. Institute of Information Security, Department of Computer Science, ETH Zürich, Zurich, Switzerland

    Andreas Lochbihler & Dmitriy Traytel

  8. Google, Zurich, Switzerland

    Fabian Meier

  9. Technische Universiteit Eindhoven, Eindhoven, The Netherlands

    Lorenz Panny

  10. Middlesex University London, London, UK

    Andrei Popescu

  11. Institute of Mathematics Simion Stoilow of the Romanian Academy, Bucharest, Romania

    Andrei Popescu

  12. Universität Innsbruck, Innsbruck, Austria

    Christian Sternagel & René Thiemann

Authors
  1. Julian Biendarra
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jasmin Christian Blanchette
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Aymeric Bouzy
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Martin Desharnais
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Mathias Fleury
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Johannes Hölzl
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Ondřej Kunčar
    View author publications

    You can also search for this author in PubMed Google Scholar

  8. Andreas Lochbihler
    View author publications

    You can also search for this author in PubMed Google Scholar

  9. Fabian Meier
    View author publications

    You can also search for this author in PubMed Google Scholar

  10. Lorenz Panny
    View author publications

    You can also search for this author in PubMed Google Scholar

  11. Andrei Popescu
    View author publications

    You can also search for this author in PubMed Google Scholar

  12. Christian Sternagel
    View author publications

    You can also search for this author in PubMed Google Scholar

  13. René Thiemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  14. Dmitriy Traytel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jasmin Christian Blanchette .

Editor information

Editors and Affiliations

  1. University of Liverpool, Liverpool, United Kingdom

    Clare Dixon

  2. University of Sao Paulo, Sao Paulo, Brazil

    Marcelo Finger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Biendarra, J. et al. (2017). Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In: Dixon, C., Finger, M. (eds) Frontiers of Combining Systems. FroCoS 2017. Lecture Notes in Computer Science(), vol 10483. Springer, Cham. https://doi.org/10.1007/978-3-319-66167-4_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66167-4_1

  • Published:

  • Publisher Name: Springer, Cham

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation