Automated Algebraic Reasoning for Collections and Local Variables with Lenses

DOI10.1007/978-3-030-43520-2_7MaRDI QIDQ5098716zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 978243
• Automated Reasoning in Kleene Algebra
• Automated reasoning in some local exensions of ordered structures
• Automated Reasoning in Higher-Order Regular Algebra
• Automatic Proof Generation in Kleene Algebra
• Automated deduction in equational logic and cubic curves
• scientific article; zbMATH DE number 1185498
• scientific article; zbMATH DE number 1303628
• scientific article; zbMATH DE number 863013

Cites work

• A program construction and verification tool for separation logic
• An algebraic treatment of procedure refinement to support mechanical verification
• An axiomatic basis for computer programming
• Building program construction and verification tools from algebraic principles
• Combinators for bi-directional tree transformations: a linguistic approach to the view update problem
• Cylindric Kleene lattices for program construction
• Guarded commands, nondeterminacy and formal derivation of programs
• scientific article; zbMATH DE number 1759984 (Why is no real title available?)
• Hybrid relations in Isabelle/UTP
• Isabelle/UTP: a mechanised theory engineering framework
• Laws of programming
• Modal Kleene algebra applied to program correctness
• On the calculus of relations
• Quotient lenses
• Refinement Calculus
• Symmetric lenses
• Unifying heterogeneous state-spaces with lenses
• Unifying theories in Isabelle/HOL
• Unifying theories of reactive design contracts
• Verifying hybrid systems with modal Kleene algebra
• Why3 -- where programs meet provers

Cited in

(1)

• IsaVODEs: Interactive verification of cyber-physical systems at scale

Describes a project that uses

Uses Software

• Boogie
• Why3
• WhyML
• Isabelle/UTP

This page was built for publication: Automated Algebraic Reasoning for Collections and Local Variables with Lenses

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5098716)