Inductive reasoning about effectful data types

DOI10.1145/1291151.1291168MaRDI QIDQ5168928zbMATH OpenOpenAlexFDO

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

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)

Recommendations

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

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)