Optics in Isabelle/HOL

Simon David Foster; Frank Zeyda

Optics in Isabelle/HOL

Computer Science

Research output: Contribution to journal › Article › peer-review

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. 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 language	English
Pages (from-to)	1-28
Number of pages	28
Journal	Archive of Formal Proofs
Publication status	Published - 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.

Access to Document

optics
© 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.
Final published version, 309 KB

https://www.isa-afp.org/entries/Optics.shtml

Cite this

@article{ad7b6e0c75074e94a8b7ac2607917f92,

title = "Optics in Isabelle/HOL",

abstract = "Lenses provide an abstract interface for manipulating data types through spatially separatedviews. 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.",

author = "Foster, {Simon David} and Frank Zeyda",

note = "{\textcopyright} 2017,The Author(s). This is an author-produced version of the published paper. Uploaded in accordance with the publisher{\textquoteright}s self-archiving policy. Further copying may not be permitted; contact the publisher for details.",

year = "2017",

month = jun,

day = "1",

language = "English",

pages = "1--28",

journal = "Archive of Formal Proofs",

}

TY - JOUR

T1 - Optics in Isabelle/HOL

AU - Foster, Simon David

AU - Zeyda, Frank

N1 - © 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.

PY - 2017/6/1

Y1 - 2017/6/1

N2 - Lenses provide an abstract interface for manipulating data types through spatially separatedviews. 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.

AB - Lenses provide an abstract interface for manipulating data types through spatially separatedviews. 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.

M3 - Article

SP - 1

EP - 28

JO - Archive of Formal Proofs

JF - Archive of Formal Proofs

ER -