Abstract: 
Lenses provide an abstract interface for manipulating data types
through spatiallyseparated 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 wellbehaved and very
wellbehaved 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. 
BibTeX: 
@article{OpticsAFP,
author = {Simon Foster and Frank Zeyda},
title = {Optics},
journal = {Archive of Formal Proofs},
month = may,
year = 2017,
note = {\url{http://isaafp.org/entries/Optics.html},
Formal proof development},
ISSN = {2150914x},
}
