A hierarchy of monadic effects for program verification using equational reasoning

DOI10.1007/978-3-030-33636-3_9MaRDI QIDQ2176680zbMATH OpenOpenAlexFDO

Authors Reynald Affeldt, Takafumi Saikawa, David Nowak

Publication date 5 May 2020

Full work available at URL https://doi.org/10.1007/978-3-030-33636-3_9

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Just do it
• Not by equations alone. Reasoning with extensible effects
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Monads in action
• Programming and reasoning with algebraic effects and dependent types

Cited in

(11)

• Modular verification of programs with effects and effects handlers
• Modular verification of programs with effects and effect handlers in Coq
• A Hoare Logic for the State Monad
• Not by equations alone. Reasoning with extensible effects
• Validating Mathematical Structures
• A trustful monad for axiomatic reasoning with probability and nondeterminism
• Just do it
• Towards a practical library for monadic equational reasoning in Coq
• Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
• A practical formalization of monadic equational reasoning in dependent-type theory
• Extending equational monadic reasoning with monad transformers

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A hierarchy of monadic effects for program verification using equational reasoning

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