Refinement Monadic
From MaRDI portal
- A Powerdomain Construction
- Code generation via higher-order rewrite systems
- Data Refinement
- Encoding, decoding and data refinement
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Imperative Functional Programming with Isabelle/HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
- Proof of correctness of data representations
- Refinement Calculus
- Refinement concepts formalised in higher order logic
- Secure Microkernels, State Monads and Scalable Refinement
- The Isabelle collections framework
Cited in
(32)- A verified ODE solver and the Lorenz attractor
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Netsoft
- Refinement to imperative HOL
- Autoref
- CFML
- MLton
- Formalizing the Edmonds-Karp algorithm
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Edmonds-Karp
- Separation Logic
- Dijkstra Shortest Path
- Flow Networks
- CAVA Automata Library
- CAVA
- Stuttering Equivalence
- Collections
- Dictionary Construction
- Affine Arithmetic
- LTL_to_DRA
- CAVA LTL Modelchecker
- Gabow SCC
- Native Word
- Imperative Refinement
- Program-Conflict-Analysis
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
- Boolean_Expression_Checkers
- Prpu_Maxflow
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- scientific article; zbMATH DE number 7649962 (Why is no real title available?)
- Transition_Systems_and_Automata
- Formal verification of an executable LTL model checker with partial order reduction
This page was built for software: Refinement Monadic
