The Isabelle collections framework

DOI10.1007/978-3-642-14052-5_24MaRDI QIDQ5747660zbMATHOpenAlexFDO

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Refinement to Imperative/HOL
• The Isabelle Framework
• Imperative Functional Programming with Isabelle/HOL
• Light-weight containers for Isabelle: efficient, extensible, nestable
• Data refinement in Isabelle/HOL

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

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Timbuk
• OCaml
• LETHAL

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)