Skip to main content
SpringerLink
Log in

Truly Modular (Co)datatypes for Isabelle/HOL

  • Conference paper
Interactive Theorem Proving (ITP 2014)

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

Included in the following conference series:

Abstract

We extended Isabelle/HOL with a pair of definitional commands for datatypes and codatatypes. They support mutual and nested (co)recursion through well-behaved type constructors, including mixed recursion–corecursion, and are complemented by syntaxes for introducing primitively (co)recursive functions and by a general proof method for reasoning coinductively. As a case study, we ported Isabelle’s Coinductive library to use the new commands, eliminating the need for tedious ad hoc constructions.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abel, A., Pientka, B.: Wellfounded recursion with copatterns: A unified approach to termination and productivity. In: Morrisett, G., Uustalu, T. (eds.) ICFP 2013, pp. 185–196. ACM (2013)

    Google Scholar 

  2. Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: A compact kernel for the calculus of inductive constructions. Sādhanā 34, 71–144 (2009)

    MATH  Google Scholar 

  3. Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: Morrisett, G., Uustalu, T. (eds.) ICFP 2013, pp. 197–208. ACM (2013)

    Google Scholar 

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

    Chapter  Google Scholar 

  5. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)

    Google Scholar 

  6. Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Formalization accompanying this paper (2014), http://www21.in.tum.de/~blanchet/codata_impl.tar.gz

  7. Blanchette, J.C., Panny, L., Popescu, A., Traytel, D.: Defining (co)datatypes in Isabelle/HOL (2014), http://isabelle.in.tum.de/dist/Isabelle/doc/datatypes.pdf

  8. Blanchette, J.C., Popescu, A., Traytel, D.: Cardinals in Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS (LNAI), vol. 8558, pp. 111–127. Springer, Heidelberg (2014)

    Google Scholar 

  9. Blanchette, J.C., Popescu, A., Traytel, D.: Witnessing (co)datatypes (2014), http://www21.in.tum.de/~blanchet/wit.pdf

  10. Danielsson, N.A., Altenkirch, T.: Subtyping, declaratively. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 100–118. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

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

    Google Scholar 

  12. Gunter, E.L.: A broader class of trees for recursive type definitions for HOL. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 141–154. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  13. Hancock, P., Ghani, N., Pattinson, D.: Representations of stream processors using nested fixed points. Log. Meth. Comput. Sci. 5(3) (2009)

    Google Scholar 

  14. Harrison, J.: Inductive definitions: Automation and application. In: Schubert, E.T., Windley, P.J., Alves-Foss, J. (eds.) TPHOLs 1995. LNCS, vol. 971, pp. 200–213. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  15. 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, Heidelberg (2013)

    Chapter  Google Scholar 

  16. Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. Bull. EATCS 62, 222–259 (1997)

    MATH  Google Scholar 

  17. Leroy, X.: A formally verified compiler back-end. J. Autom. Reas. 43(4), 363–446 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  18. Lochbihler, A.: Coinductive. In: Klein, G., Nipkow, T., Paulson, L. (eds.) Archive of Formal Proofs (2010), http://afp.sf.net/entries/Coinductive.shtml

  19. Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427–447. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  20. Lochbihler, A.: A Machine-Checked, Type-Safe Model of Java Concurrency: Language, Virtual Machine, Memory Model, and Verified Compiler. Ph.D. thesis, Karlsruher Institut für Technologie (2012)

    Google Scholar 

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

    Google Scholar 

  22. Lochbihler, A., Hölzl, J.: Recursive functions on lazy lists via domains and topologies. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS (LNAI), vol. 8558, pp. 341–357. Springer, Heidelberg (2014)

    Google Scholar 

  23. Melham, T.F.: Automating recursive type definitions in higher order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automated Theorem Proving, pp. 341–386. Springer (1989)

    Google Scholar 

  24. Nipkow, T., Klein, G.: Concrete Semantics: A Proof Assistant Approach. Springer (to appear), http://www.in.tum.de/~nipkow/Concrete-Semantics

  25. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    Book  Google Scholar 

  26. Owre, S., Shankar, N.: A brief overview of PVS. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 22–27. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  27. Panny, L.: Primitively (Co)recursive Function Definitions for Isabelle/HOL. B.Sc. thesis draft, Technische Universität München (2014)

    Google Scholar 

  28. Paulson, L.C.: A fixedpoint approach to implementing (co)inductive definitions. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 148–161. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  29. Paulson, L.C.: Mechanizing coinduction and corecursion in higher-order logic. J. Log. Comput. 7(2), 175–204 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  30. Rutten, J.J.M.M.: Universal coalgebra: A theory of systems. Theor. Comput. Sci. 249, 3–80 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  31. Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle/HOL: Animating a many-sorted metatheory. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 114–130. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  32. Traytel, D.: A Category Theory Based (Co)datatype Package for Isabelle/HOL. M.Sc. thesis, Technische Universität München (2012)

    Google Scholar 

  33. 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 (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Jasmin Christian Blanchette, Johannes Hölzl, Lorenz Panny, Andrei Popescu & Dmitriy Traytel

  2. Institute of Information Security, ETH Zurich, Switzerland

    Andreas Lochbihler

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

    Andrei Popescu

Authors
  1. Jasmin Christian Blanchette
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Johannes Hölzl
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andreas Lochbihler
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lorenz Panny
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Andrei Popescu
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Dmitriy Traytel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NICTA, Sydney, NSW, Australia

    Gerwin Klein

  2. University of Wyoming, Laramie, WY, USA

    Ruben Gamboa

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D. (2014). Truly Modular (Co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08970-6_7

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08969-0

  • Online ISBN: 978-3-319-08970-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation