package coq-continuations

  1. Overview
  2. Homepage
A toolkit to reason with programs raising exceptions

Install

Dune Dependency

Authors

Maintainers

Sources

v8.7.0.tar.gz
md5=1a6170334b8f2b0dbd73386952cb2d83

Description

We show a way of developing correct functionnal programs raising exceptions. This is made possible using a Continuation Passing Style translation, see the contribution "exceptions" from P. Casteran at Bordeaux. Things are made easier and more modular using some general definitions.

Dependencies (2)

  1. coq >= "8.7" & < "8.8~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover