Modular verification of programs with effects and effect handlers in Coq

DOI10.1007/978-3-319-95582-7_20zbMath1460.68062OpenAlexW2807309257MaRDI QIDQ2024352

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

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)

Related Items (1)

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

Uses Software

• Unnamed Item

Cites Work

• Unnamed Item
• Programming with algebraic effects and handlers
• Termination Proofs for Recursive Functions in FoCaLiZe
• Coquet: A Coq Library for Verifying Hardware
• The B-Book
• Ynot

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