Extensional equality preservation and verified generic programming
From MaRDI portal
Publication:5019020
DOI10.1017/S0956796821000204OpenAlexW3211048084MaRDI QIDQ5019020
Nuria Brede, Tim Richter, Patrik Jansson, Nicola Botta
Publication date: 27 December 2021
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2008.02123
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Elements of applied bifurcation theory.
- Polytypic data conversion programs
- Proving type class laws for Haskell
- Algebra of programming in Agda: Dependent types for relational program derivation
- Dynamic Programming as Graph Searching: An Algebraic Approach
- Contributions to a computational theory of policy advice and avoidability
- Cubical Type Theory: a constructive interpretation of the univalence axiom
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- On the correctness of monadic backward induction
- Fast and loose reasoning is morally correct
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Applicative programming with effects
- Realms: A Structure for Consolidating Knowledge about Mathematical Theories
- FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell
This page was built for publication: Extensional equality preservation and verified generic programming