Imperative Functional Programming with Isabelle/HOL
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 2086515 (Why is no real title available?)
- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
- Efficiently checking propositional refutations in HOL theorem provers
- HOLCF = HOL + LCF
- Logic for Programming, Artificial Intelligence, and Reasoning
- Partizan Games in Isabelle/HOLZF
- Polymorphism and separation in Hoare type theory
- Theorem Proving in Higher Order Logics
- Theory and Applications of Satisfiability Testing
- Types, bytes, and separation logic
Cited in
(51)- Comprehending Isabelle/HOL’s Consistency
- Proving pointer programs in higher-order logic.
- iRho: an imperative rewriting calculus
- Proof-producing synthesis of CakeML from monadic HOL functions
- Implementing hybrid semantics: from functional to imperative
- A proof tool for reasoning about functional programs
- Refinement to imperative HOL
- The Isabelle collections framework
- scientific article; zbMATH DE number 1420787 (Why is no real title available?)
- A language-based approach to functionally correct imperative programming
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- The Isabelle Framework
- Efficient verified (UN)SAT certificate checking
- A framework for the verification of certifying computations
- Translating Scala programs to Isabelle/HOL. System description
- Building program construction and verification tools from algebraic principles
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
- Functional data structures and algorithms. A proof assistant approach
- Trace-based verification of imperative programs with I/O
- Trustworthy Graph Algorithms (Invited Talk)
- Implementing and reasoning about hash-consed data structures in Coq
- Theorem Proving in Higher Order Logics
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Refinement to Imperative/HOL
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Verification and code generation for invariant diagrams in Isabelle
- Equational Reasoning with Applicative Functors
- Concrete semantics. With Isabelle/HOL
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
- Simplified and verified: a second look at a proof-producing union-find algorithm
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
- From LCF to Isabelle/HOL
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- Effect polymorphism in higher-order logic (proof pearl)
- Effect polymorphism in higher-order logic (proof pearl)
- Practical Tactics for Separation Logic
- Proving pointer programs in higher-order logic
- Executing and verifying higher-order functional-imperative programs in Maude
- A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL
- Effective interactive proofs for higher-order imperative programs
- Animating the formalised semantics of a Java-like language
- Verified certification of reachability checking for timed automata
- Verified memoization and dynamic programming
- Verification of the Schorr-Waite algorithm -- from trees to graphs
- AUTO2, a saturation-based heuristic prover for higher-order logic
- scientific article; zbMATH DE number 7649969 (Why is no real title available?)
- Formalizing the Edmonds-Karp algorithm
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Light-weight containers for Isabelle: efficient, extensible, nestable
This page was built for publication: Imperative Functional Programming with Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543655)
