Title: Optics
Authors: Simon Foster and Frank Zeyda
Submission date: 2017-05-25
Abstract: 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.
Change history: [2020-03-02]: Added partial bijective and symmetric lenses. Improved alphabet command generating additional lenses and results. Several additional lens relations, including observational equivalence. Additional theorems throughout. Adaptations for Isabelle 2020. (revision 44e2e5c)
  author  = {Simon Foster and Frank Zeyda},
  title   = {Optics},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2017,
  note    = {\url{https://isa-afp.org/entries/Optics.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License