Email Gateway (May 24 2025 at 18:39): Email Gateway (May 24 2025 at 18:39):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
A new AFP entry by Simon Foster:
Shallow Expressions
Most verification techniques use expressions, for example when assigning to variables or forming assertions over the state. Deep embeddings provide such expressions using a datatype, which allows queries over the syntax, such as calculating the free variables, and performing substitutions. Shallow embeddings, in contrast, model expressions as query functions over the state type, and are more amenable to automating verification tasks. The goal of this library is provide an intuitive implementation of shallow expressions, which nevertheless provides many of the benefits of a deep embedding. We harness the Optics library to provide an algebraic semantics for state variables, and use syntax translations to provide an intuitive lifted expression syntax. Furthermore, we provide a variety of meta-logic-style queries on expressions, such as dependencies on a state variable, and substitution of a variable for an expression. We also provide proof methods, based on the simplifier, to automate the associated proof tasks.
https://www.isa-afp.org/entries/Shallow_Expressions.html
Enjoy!
Last updated: May 30 2025 at 04:27 UTC