Extending equational monadic reasoning with monad transformers

DOI10.4230/LIPICS.TYPES.2020.2MaRDI QIDQ7232179zbMATH OpenFDO

Authors Reynald Affeldt, David Nowak

Publication date 22 April 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.TYPES.2020.2

zbMATH Keywords

Coqimpredicativitymonad transformersmonadsparametricity

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites work

• A computational interpretation of parametricity
• A hierarchy of monadic effects for program verification using equational reasoning
• A relationally parametric model of dependent type theory
• Declarative pearl: deriving monadic quicksort
• Formal verification of monad transformers
• Handling local state with global state
• scientific article; zbMATH DE number 7204300 (Why is no real title available?)
• Internalizing relational parametricity in the extensional calculus of constructions
• Just do it
• Logical relations for monadic types
• Modular Monad Transformers
• Monad transformers as monoid transformers
• Packaging Mathematical Structures
• Parametricity in an impredicative sort
• Unifying theories of programming with monads

This page was built for publication: Extending equational monadic reasoning with monad transformers

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