Light-weight containers for Isabelle: efficient, extensible, nestable

DOI10.1007/978-3-642-39634-2_11MaRDI QIDQ5327340zbMATH OpenOpenAlexFDO

Authors Andreas Lochbihler

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39634-2_11

Mathematics Subject Classification ID

Recommendations

• The Isabelle collections framework
• Data refinement in Isabelle/HOL
• Constructive Type Classes in Isabelle
• The Isabelle Framework
• Imperative Functional Programming with Isabelle/HOL

Cited in

(21)

• A consistent foundation for Isabelle/HOL
• Isabelle's metalogic: formalization and proof checker
• A formally verified, optimized monitor for metric first-order dynamic logic
• A formalization and proof checker for Isabelle's metalogic
• Certifying proofs in the first-order theory of rewriting
• Automatic refinement to efficient data structures: a comparison of two approaches
• More SPASS with Isabelle
• A consistent foundation for Isabelle/HOL
• Deriving comparators and show functions in Isabelle/HOL
• Correct code containing containers
• Formalization and execution of linear algebra: from theorems to algorithms
• Deriving class
• Datatype Order Generator
• Light-weight Containers
• Real_Impl
• Reachability, confluence, and termination analysis with state-compatible automata
• The Isabelle collections framework
• AI Planning Languages Semantics
• Verified SAT-Based AI Planning
• Upper Bounding Diameters of State Spaces of Factored Transition Systems
• A Formal CHERI-C Memory Model

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• FinFuns
• Containers
• Datatype Order Generator

This page was built for publication: Light-weight containers for Isabelle: efficient, extensible, nestable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327340)