Automated Algebraic Reasoning for Collections and Local Variables with Lenses

DOI10.1007/978-3-030-43520-2_7OpenAlexW3012993020MaRDI QIDQ5098716

Simon Foster, James Baxter

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

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Why3
• Boogie
• WhyML
• Isabelle/UTP

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