Extensional equality preservation and verified generic programming

Nicola Botta, Nuria Brede, Patrik Jansson & Tim Richter
In verified generic programming, one cannot exploit the structure of concrete data types but has
to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads
are at the core of many applications of functional programming. This raises the question of what
useful ADTs for verified functors and monads could look like. The functorial map of many important
monads preserves extensional equality. For instance, if f , g : A...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.