Modular verification of programs with effects and effect handlers in Coq

DOI10.1007/978-3-319-95582-7_20MaRDI QIDQ2024352zbMATH OpenOpenAlexFDO

Authors Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet

Publication date 4 May 2021

Full work available at URL https://hal.inria.fr/hal-01799712/file/main.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Modular verification of programs with effects and effects handlers
• Modular development of certified program verifiers with a proof assistant,
• Effective interactive proofs for higher-order imperative programs
• A hierarchy of monadic effects for program verification using equational reasoning
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)

Cites work

• Coquet: a Coq library for verifying hardware
• Programming with algebraic effects and handlers
• Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell
• Termination Proofs for Recursive Functions in FoCaLiZe
• The B-Book
• Ynot: dependent types for imperative programs

Cited in

(4)

• Modular verification of programs with effects and effects handlers
• Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
• A practical formalization of monadic equational reasoning in dependent-type theory
• Choice trees: representing and reasoning about nondeterministic, recursive, and impure programs in Rocq

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Modular verification of programs with effects and effect handlers in Coq

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