Truly modular (co)datatypes for Isabelle/HOL
From MaRDI portal
Recommendations
- Foundational (co)datatypes and (co)recursion for higher-order logic
- Witnessing (co)datatypes
- Foundational nonuniform (co)datatypes for higher-order logic
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Mechanizing coinduction and corecursion in higher-order logic
Cited in
(46)- CoSMed: a confidentiality-verified social media platform
- Formalization of the resolution calculus for first-order logic
- Foundational (co)datatypes and (co)recursion for higher-order logic
- A formalized general theory of syntax with bindings
- Markov chains and Markov decision processes in Isabelle/HOL
- Relational parametricity and quotient preservation for modular (co)datatypes
- A formalized general theory of syntax with bindings: extended version
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL
- Non-well-founded deduction for induction and coinduction
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- CryptHOL: game-based proofs in higher-order logic
- Deep induction: induction rules for (truly) nested types
- Interactive verification of architectural design patterns in FACTum
- A decision procedure for (co)datatypes in SMT solvers
- Soundness and completeness proofs by coinductive methods
- Automatic refinement to efficient data structures: a comparison of two approaches
- Witnessing (co)datatypes
- Probabilistic functions and cryptographic oracles in higher order logic
- Translating Scala programs to Isabelle/HOL. System description
- Modular dependent induction in Coq, Mendler-style
- Nonfree datatypes in Isabelle/HOL. Animating a many-sorted metatheory
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- A formalized hierarchy of probabilistic system types. Proof pearl
- Deriving comparators and show functions in Isabelle/HOL
- Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
- Friends with benefits. Implementing corecursion in foundational proof assistants
- Quotients of Bounded Natural Functors
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- Foundational nonuniform (co)datatypes for higher-order logic
- Coinduction in Flow: The Later Modality in Fibrations
- scientific article; zbMATH DE number 7649955 (Why is no real title available?)
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- scientific article; zbMATH DE number 7649978 (Why is no real title available?)
- Effect polymorphism in higher-order logic (proof pearl)
- A comprehensive framework for saturation theorem proving
- Effect polymorphism in higher-order logic (proof pearl)
- A comprehensive framework for saturation theorem proving
- Formalising Mathematics in Simple Type Theory
- Into the Infinite - Theory Exploration for Coinduction
- Proofs about Network Communication: For Humans and Machines
- Linear resources in Isabelle/HOL
- Formal verification of an executable LTL model checker with partial order reduction
- A contextual formalization of structural coinduction
- Abstract, compositional consistency: Isabelle/HOL locales for completeness à la fitting
- Animating MRBNFs: truly modular binding-aware datatypes in Isabelle/HOL
- Nondeterministic asynchronous dataflow in Isabelle/HOL
Describes a project that uses
Uses Software
This page was built for publication: Truly modular (co)datatypes for Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879246)
