A hierarchy of monadic effects for program verification using equational reasoning

DOI10.1007/978-3-030-33636-3_9zbMath1434.68100OpenAlexW2980486477MaRDI QIDQ2176680

Reynald Affeldt, Takafumi Saikawa, David E. 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) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Validating Mathematical Structures ⋮ Towards a practical library for monadic equational reasoning in Coq ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism

Uses Software

• Coq

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