The Isabelle collections framework
From MaRDI portal
Publication:5747660
DOI10.1007/978-3-642-14052-5_24zbMATH Open1291.68357OpenAlexW1581325065MaRDI QIDQ5747660FDOQ5747660
Authors: Peter Lammich, Andreas Lochbihler 
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_24
Recommendations
Cited In (17)
- Formal verification of an executable LTL model checker with partial order reduction
- Efficient verified (UN)SAT certificate checking
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- The Isabelle Framework
- Mining the Archive of Formal Proofs
- Deriving Comparators and Show Functions in Isabelle/HOL
- Gale-Shapley verified
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Refinement to Imperative/HOL
- Isabelle's metalogic: formalization and proof checker
- A formalization and proof checker for Isabelle's metalogic
- Automatic refinement to efficient data structures: a comparison of two approaches
- Animating the formalised semantics of a Java-like language
- Verified synthesis of knowledge-based programs in finite synchronous environments
- Reachability, confluence, and termination analysis with state-compatible automata
- Light-weight containers for Isabelle: efficient, extensible, nestable
- Verified efficient enumeration of plane graphs modulo isomorphism
Uses Software
This page was built for publication: The Isabelle collections framework
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747660)
