The Isabelle Collections Framework
From MaRDI portal
Publication:5747660
DOI10.1007/978-3-642-14052-5_24zbMath1291.68357OpenAlexW1581325065MaRDI QIDQ5747660
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
Related Items
Mining the Archive of Formal Proofs, Refinement to Imperative/HOL, Deriving Comparators and Show Functions in Isabelle/HOL, Automatic refinement to efficient data structures: a comparison of two approaches, Formal verification of an executable LTL model checker with partial order reduction, Reachability, confluence, and termination analysis with state-compatible automata, Efficient verified (UN)SAT certificate checking, 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, Isabelle's metalogic: formalization and proof checker, A formalization and proof checker for Isabelle's metalogic
Uses Software
