Extensional equality preservation and verified generic programming

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (1)

On the correctness of monadic backward induction

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