Modular verification of programs with effects and effects handlers
DOI10.1007/S00165-020-00523-2zbMATH Open1458.68119OpenAlexW3110742659MaRDI QIDQ1996433FDOQ1996433
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
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
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- The power of parameterization in coinductive proof
- Ynot: dependent types for imperative programs
- Programming with algebraic effects and handlers
- Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell
- Comprehending monads
- Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 -- July 1, 2015. Proceedings
- Container combinatorics: monads and lax monoidal functors
- Coquet: a Coq library for verifying hardware
Cited In (11)
- Modular correctness proofs of behavioural implementations
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
Uses Software
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)
