Modular verification of programs with effects and effects handlers

DOI10.1007/S00165-020-00523-2zbMath1458.68119OpenAlexW3110742659MaRDI QIDQ1996433

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

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

formal verificationCoq

Mathematics Subject Classification ID

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

Related Items (1)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Uses Software

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

Cites Work

• Unnamed Item
• Programming with algebraic effects and handlers
• Container combinatorics: monads and lax monoidal functors
• Mathematics of program construction. 12th international conference, MPC 2015, Königswinter, Germany, June 29 -- July 1, 2015. Proceedings
• The power of parameterization in coinductive proof
• Coquet: A Coq Library for Verifying Hardware
• Comprehending monads
• Ynot

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