|
Optics
Title: |
Optics |
Authors:
|
Simon Foster (simon /dot/ foster /at/ york /dot/ ac /dot/ uk) and
Frank Zeyda (frank /dot/ zeyda /at/ york /dot/ ac /dot/ uk)
|
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. |
BibTeX: |
@article{Optics-AFP,
author = {Simon Foster and Frank Zeyda},
title = {Optics},
journal = {Archive of Formal Proofs},
month = may,
year = 2017,
note = {\url{http://isa-afp.org/entries/Optics.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|