Automated Algebraic Reasoning for Collections and Local Variables with Lenses
From MaRDI portal
Publication:5098716
DOI10.1007/978-3-030-43520-2_7OpenAlexW3012993020MaRDI QIDQ5098716
Publication date: 30 August 2022
Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://eprints.whiterose.ac.uk/155413/15/RAMiCS2020.pdf
Uses Software
Cites Work
- Unnamed Item
- Building program construction and verification tools from algebraic principles
- Verifying hybrid systems with modal Kleene algebra
- Unifying theories of reactive design contracts
- Cylindric Kleene lattices for program construction
- Modal Kleene algebra applied to program correctness
- Hybrid relations in Isabelle/UTP
- An algebraic treatment of procedure refinement to support mechanical verification
- Isabelle/UTP: A Mechanised Theory Engineering Framework
- A Program Construction and Verification Tool for Separation Logic
- Unifying Theories in Isabelle/HOL
- Unifying Heterogeneous State-Spaces with Lenses
- Laws of programming
- Guarded commands, nondeterminacy and formal derivation of programs
- Refinement Calculus
- Quotient lenses
- Combinators for bi-directional tree transformations
- Why3 — Where Programs Meet Provers
- Symmetric lenses
- An axiomatic basis for computer programming
- On the calculus of relations
This page was built for publication: Automated Algebraic Reasoning for Collections and Local Variables with Lenses
