Inductive reasoning about effectful data types

DOI10.1145/1291151.1291168zbMATH Open1291.68143OpenAlexW2106256381MaRDI QIDQ5168928FDOQ5168928

Authors: Andrzej Filinski, Kristian Støvring 

Publication date: 21 July 2014

Published in: Proceedings of the 12th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1291151.1291168

Recommendations

• Fibrational induction meets effects
• Interleaving data and effects
• Not by equations alone. Reasoning with extensible effects
• State will do
• Just do it

zbMATH Keywords

monadsbacktrackinglogical relationsrecursive typesequational reasoningstreamsabstract effects

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Cited In (7)

• Monads for behaviour
• Inductive data types for predicate transformers
• The coinductive resumption monad
• Codensity lifting of monads and its dual
• Relating Computational Effects by ⊤ ⊤-Lifting
• Interleaving data and effects
• Eilenberg-Moore monoids and backtracking monad transformers

This page was built for publication: Inductive reasoning about effectful data types

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