Isabelle Coinductive: This article collects formalisations of general-purpose coinductive data types and sets. Currently, it contains coinductive natural numbers, coinductive lists, i.e. lazy lists or streams, infinite streams, coinductive terminated lists, coinductive resumptions, a library of operations on coinductive lists, and a version of König’s lemma as an application for coinductive lists. The initial theory was contributed by Paulson and Wenzel. Extensions and other coinductive formalisations of general interest are welcome.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Rusu, Vlad; Nowak, David: (Co)inductive proof systems for compositional proofs in reachability logic (2021)
- Marmsoler, Diego; Gidey, Habtom Kashay: Interactive verification of architectural design patterns in FACTum (2019)
- Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
- Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy: Foundational (co)datatypes and (co)recursion for higher-order logic (2017)
- Åman Pohjola, Johannes; Parrow, Joachim: The expressive power of monotonic parallel composition (2016)
- Blanchette, Jasmin Christian; Hölzl, Johannes; Lochbihler, Andreas; Panny, Lorenz; Popescu, Andrei; Traytel, Dmitriy: Truly modular (co)datatypes for Isabelle/HOL (2014)
- Lochbihler, Andreas; Hölzl, Johannes: Recursive functions on lazy lists via domains and topologies (2014)