Pages that link to "Item:Q3543655"
From MaRDI portal
The following pages link to Imperative Functional Programming with Isabelle/HOL (Q3543655):
Displaying 31 items.
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Building program construction and verification tools from algebraic principles (Q736461) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL (Q1722647) (← links)
- Refinement to imperative HOL (Q1739909) (← links)
- Implementing hybrid semantics: from functional to imperative (Q2037951) (← links)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- A framework for the verification of certifying computations (Q2351144) (← links)
- Implementing and reasoning about hash-consed data structures in Coq (Q2351422) (← links)
- Formalizing the Edmonds-Karp Algorithm (Q2829260) (← links)
- Equational Reasoning with Applicative Functors (Q2829262) (← links)
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic (Q2829278) (← links)
- Refinement to Imperative/HOL (Q2945637) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- Verification of the Schorr-Waite Algorithm – From Trees to Graphs (Q3003486) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- Practical Tactics for Separation Logic (Q3183539) (← links)
- iRho: an imperative rewriting calculus (Q3520144) (← links)
- The Isabelle Framework (Q3543647) (← links)
- Verified Certification of Reachability Checking for Timed Automata (Q5039522) (← links)
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation (Q5049007) (← links)
- Trustworthy Graph Algorithms (Invited Talk) (Q5092359) (← links)
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm (Q5371950) (← links)
- (Q5875428) (← links)
- (Q5875431) (← links)
- Effect polymorphism in higher-order logic (proof pearl) (Q5915785) (← links)
- Efficient verified (UN)SAT certificate checking (Q5919480) (← links)
- Effect polymorphism in higher-order logic (proof pearl) (Q5919584) (← links)
- Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding (Q6611968) (← links)
