The Isabelle Collections Framework
From MaRDI portal
Publication:5747660
DOI10.1007/978-3-642-14052-5_24zbMath1291.68357MaRDI 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
68N18: Functional programming and lambda calculus
Related Items
Efficient verified (UN)SAT certificate checking, Reachability, confluence, and termination analysis with state-compatible automata, Formal verification of an executable LTL model checker with partial order reduction, 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, Mining the Archive of Formal Proofs
Uses Software