Optics

MaRDI QIDQ7361308FDO

Authors Simon Foster, Christian Pardillo-Laursen, Frank Zeyda

Publication date 25 May 2017

Cites work

• A clear picture of lens laws
• A program construction and verification tool for separation logic
• A UTP semantics for \textsf{Circus}
• An Axiomatic Value Model for Isabelle/UTP
• Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
• Automated Reasoning in Higher-Order Regular Algebra
• Automatic proof and disproof in Isabelle/HOL
• Building program construction and verification tools from algebraic principles
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/UTP: a mechanised theory engineering framework
• Laws of programming
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• On the calculus of relations
• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Refinement Calculus
• Symmetric lenses
• Towards a UTP semantics for Modelica
• Unifying heterogeneous state-spaces with lenses
• Unifying theories in Isabelle/HOL
• Unifying Theories in ProofPower-Z

Cited in

(4)

• ConcurrentHOL
• Shallow Expressions
• Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
• Z Mathematical Toolkit in Isabelle/HOL

This page was built for software: Optics