The Isabelle collections framework
From MaRDI portal
Publication:5747660
Recommendations
Cited in
(19)- Mining the Archive of Formal Proofs
- Gale-Shapley verified
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Light-weight containers for Isabelle: efficient, extensible, nestable
- Isabelle's metalogic: formalization and proof checker
- Refinement to Imperative/HOL
- Verified synthesis of knowledge-based programs in finite synchronous environments
- Animating the formalised semantics of a Java-like language
- Fast machine words in Isabelle/HOL
- Formal verification of an executable LTL model checker with partial order reduction
- Efficient verified (UN)SAT certificate checking
- Automatic refinement to efficient data structures: a comparison of two approaches
- A formalization and proof checker for Isabelle's metalogic
- Reachability, confluence, and termination analysis with state-compatible automata
- Verified efficient enumeration of plane graphs modulo isomorphism
- Verified memoization and dynamic programming
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Deriving comparators and show functions in Isabelle/HOL
- The Isabelle Framework
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)