Extensional equality preservation and verified generic programming

DOI10.1017/S0956796821000204MaRDI QIDQ5019020zbMATH OpenOpenAlexFDO

Authors Nuria Brede, Patrik Jansson, Tim Richter, N. Botta

Publication date 27 December 2021

Published in Journal of Functional Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2008.02123

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• On monadic parametricity of second-order functionals
• Formal verification of monad transformers
• Programming Languages and Systems
• Formal polytypic programs and proofs
• Parametricity, type equality, and higher-order polymorphism

Cites work

• A new look at generalized rewriting in type theory
• Algebra of programming in Agda: Dependent types for relational program derivation
• Applicative programming with effects
• Contributions to a computational theory of policy advice and avoidability
• Cubical Agda: a dependently typed programming language with univalence and higher inductive types
• Cubical type theory: a constructive interpretation of the univalence axiom
• Dynamic Programming as Graph Searching: An Algebraic Approach
• Elements of applied bifurcation theory.
• Fast and loose reasoning is morally correct
• FUNCTIONAL PEARLS: Probabilistic functional programming in Haskell
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3126094 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3764843 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 107664 (Why is no real title available?)
• scientific article; zbMATH DE number 3549200 (Why is no real title available?)
• scientific article; zbMATH DE number 977284 (Why is no real title available?)
• scientific article; zbMATH DE number 6981655 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• scientific article; zbMATH DE number 3291139 (Why is no real title available?)
• On the correctness of monadic backward induction
• Polytypic data conversion programs
• Proving type class laws for Haskell
• Realms: a structure for consolidating knowledge about mathematical theories

Cited in

(4)

• Partial type equivalences for verified dependent interoperability
• scientific article; zbMATH DE number 683355 (Why is no real title available?)
• On the correctness of monadic backward induction
• A well-known representation of monoids and its application to the function ‘vector reverse’

This page was built for publication: Extensional equality preservation and verified generic programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5019020)