The Isabelle collections framework
From MaRDI portal
Recommendations
Cited in
(31)- Fast machine words in Isabelle/HOL
- Verified memoization and dynamic programming
- 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
- Refinement to Imperative/HOL
- Deriving comparators and show functions in Isabelle/HOL
- Verified synthesis of knowledge-based programs in finite synchronous environments
- Animating the formalised semantics of a Java-like language
- Verified efficient enumeration of plane graphs modulo isomorphism
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Mining the Archive of Formal Proofs
- The Isabelle Framework
- Edmonds-Karp
- Separation Logic
- Dijkstra Shortest Path
- Refinement Monadic
- Flow Networks
- KBPs
- Deriving class
- Datatype Order Generator
- Collections
- Gabow SCC
- Light-weight Containers
- Reachability, confluence, and termination analysis with state-compatible automata
- Light-weight containers for Isabelle: efficient, extensible, nestable
- Prpu_Maxflow
- Efficient verified (UN)SAT certificate checking
- Gale-Shapley verified
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Formal verification of an executable LTL model checker with partial order reduction
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)
