Email Gateway (Aug 22 2022 at 15:33): Email Gateway (Aug 22 2022 at 15:33):From: Gerwin.Klein@data61.csiro.au
A new entry is available in the AFP:
Optics
by Simon Foster and Frank Zeyda
Lenses provide an abstract interface for manipulating data types through spatially-separated views. They are defined abstractly in terms of two functions, get, the return a value from the source type, and put that updates the value. We mechanise the underlying theory of lenses, in terms of an algebraic hierarchy of lenses, including well-behaved and very well-behaved lenses, each lens class being characterised by a set of lens laws. We also mechanise a lens algebra in Isabelle that enables their composition and comparison, so as to allow construction of complex lenses. This is accompanied by a large library of algebraic laws. Moreover we also show how the lens classes can be applied by instantiating them with a number of Isabelle data types. This theory development is based on our recent work, which shows how lenses can be used to unify heterogeneous representations of state-spaces in formalised programs.
https://www.isa-afp.org/entries/Optics.shtml
Enjoy!
Gerwin
Last updated: Apr 20 2024 at 04:19 UTC