Truly Modular (Co)datatypes for Isabelle/HOL
From MaRDI portal
Publication:2879246
DOI10.1007/978-3-319-08970-6_7zbMath1416.68151OpenAlexW2152762348MaRDI QIDQ2879246
Jasmin Christian Blanchette, Lorenz Panny, Johannes Hölzl, Dmitriy Traytel, Andrei Popescu, Andreas Lochbihler
Publication date: 8 September 2014
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://eprints.mdx.ac.uk/15167/1/codat-impl.pdf
Related Items (33)
A decision procedure for (co)datatypes in SMT solvers ⋮ Soundness and completeness proofs by coinductive methods ⋮ Quotients of Bounded Natural Functors ⋮ CoSMed: a confidentiality-verified social media platform ⋮ Formalization of the resolution calculus for first-order logic ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ Deriving Comparators and Show Functions in Isabelle/HOL ⋮ Automatic refinement to efficient data structures: a comparison of two approaches ⋮ A formalized general theory of syntax with bindings ⋮ Formalising Mathematics in Simple Type Theory ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Proofs about Network Communication: For Humans and Machines ⋮ Deep induction: induction rules for (truly) nested types ⋮ Markov chains and Markov decision processes in Isabelle/HOL ⋮ Friends with Benefits ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ Formal verification of an executable LTL model checker with partial order reduction ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Effect polymorphism in higher-order logic (proof pearl) ⋮ Probabilistic Functions and Cryptographic Oracles in Higher Order Logic ⋮ A comprehensive framework for saturation theorem proving ⋮ Unnamed Item ⋮ Translating Scala Programs to Isabelle/HOL ⋮ Non-well-founded deduction for induction and coinduction ⋮ Interactive verification of architectural design patterns in FACTum ⋮ A comprehensive framework for saturation theorem proving ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
Uses Software
This page was built for publication: Truly Modular (Co)datatypes for Isabelle/HOL
