Modular verification of programs with effects and effects handlers

DOI10.1007/S00165-020-00523-2MaRDI QIDQ1996433zbMATH OpenOpenAlexFDO

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

Publication date 4 March 2021

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-020-00523-2

zbMATH Keywords

Coqformal verification

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 effect handlers in Coq
• scientific article; zbMATH DE number 176727
• Modular verification for shared-variable concurrent programs
• Modular development of certified program verifiers with a proof assistant,
• A hierarchy of monadic effects for program verification using equational reasoning

Cites work

• Comprehending monads
• Container combinatorics: monads and lax monoidal functors
• Coquet: a Coq library for verifying hardware
• Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 -- July 1, 2015. Proceedings
• Programming with algebraic effects and handlers
• Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell
• The power of parameterization in coinductive proof
• Ynot: dependent types for imperative programs

Cited in

(11)

• Modular correctness proofs of behavioural implementations
• scientific article; zbMATH DE number 1487634 (Why is no real title available?)
• Sound, modular and compositional verification of the input/output behavior of programs
• Lightweight static capabilities
• Modular verification of programs with effects and effect handlers in Coq
• Context-Sensitive Multivariant Assertion Checking in Modular Programs
• Automated temporal verification for algebraic effects
• Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
• Modular inference of subprogram contracts for safety checking
• scientific article; zbMATH DE number 7566074 (Why is no real title available?)
• A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols

Describes a project that uses

Uses Software

• FreeSpec
• operational
• GitHub
• Kami
• Rocksalt
• Eff
• FoCaLiZe
• Paco
• Coquet
• ESC/Java
• Spec#
• Haskell
• Coq

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

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