Imperative Functional Programming with Isabelle/HOL

DOI10.1007/978-3-540-71067-7_14zbMath1165.68352OpenAlexW1522519483MaRDI QIDQ3543655

No author found.

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_14

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Verified Certification of Reachability Checking for Timed Automata, Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation, Practical Tactics for Separation Logic, A verified SAT solver framework with learn, forget, restart, and incrementality, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Refinement to Imperative/HOL, Trace-based verification of imperative programs with I/O, A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL, Unnamed Item, Unnamed Item, Proof-producing synthesis of CakeML from monadic HOL functions, Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Comprehending Isabelle/HOL’s Consistency, The Isabelle Framework, Verification of the Schorr-Waite Algorithm – From Trees to Graphs, Refinement to imperative HOL, Effect polymorphism in higher-order logic (proof pearl), From LCF to Isabelle/HOL, Effect polymorphism in higher-order logic (proof pearl), Building program construction and verification tools from algebraic principles, Efficient verified (UN)SAT certificate checking, Animating the Formalised Semantics of a Java-Like Language, Trustworthy Graph Algorithms (Invited Talk), Formalizing the Edmonds-Karp Algorithm, Equational Reasoning with Applicative Functors, AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic, A framework for the verification of certifying computations, Implementing and reasoning about hash-consed data structures in Coq

Uses Software

• Isabelle
• MiniSat
• Isabelle/HOL
• KRAKATOA
• Why3
• Caduceus

Cites Work

• Unnamed Item
• Efficiently checking propositional refutations in HOL theorem provers
• Types, bytes, and separation logic
• A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
• Partizan Games in Isabelle/HOLZF
• HOLCF = HOL + LCF
• Theory and Applications of Satisfiability Testing
• Theorem Proving in Higher Order Logics
• Polymorphism and separation in hoare type theory
• Logic for Programming, Artificial Intelligence, and Reasoning