Optics in Isabelle/HOL

Research output: Contribution to journalArticlepeer-review


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 paper, which shows how lenses can be used to unify heterogeneous representations of state-spaces in formalised programs.
Original languageEnglish
Pages (from-to)1-28
Number of pages28
JournalArchive of Formal Proofs
Publication statusPublished - 1 Jun 2017

Bibliographical note

© 2017,The Author(s). This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

Cite this