Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
From MaRDI portal
- A practical theory of programming
- An axiomatic basis for computer programming
- An Axiomatic Value Model for Isabelle/UTP
- Automated Reasoning in Higher-Order Regular Algebra
- Automatic proof and disproof in Isabelle/HOL
- Building program construction and verification tools from algebraic principles
- Calculational verification of reactive programs with reactive relations and Kleene algebra
- Guarded commands, nondeterminacy and formal derivation of programs
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Integrated Formal Methods
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Isabelle/UTP: a mechanised theory engineering framework
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Predicative programming Part I
- Program analysis and verification based on Kleene algebra in Isabelle/HOL
- Refinement Calculus
- Termination conventions and comparative semantics
- Unifying heterogeneous state-spaces with lenses
- Unifying theories in Isabelle/HOL
- Unifying Theories in ProofPower-Z
This page was built for software: Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
