package coq-classical-realizability

  1. Overview
  2. No Docs
Krivine's classical realizability

Install

Dune Dependency

Authors

Maintainers

Sources

v8.9.0.tar.gz
md5=59773d429c7003f5ff88bc4984521453

Description

The aim of this Coq library is to provide a framework for checking proofs in Krivine's classical realizability for second-order Peano arithmetic.

It is designed to be as extensible as the original theory by Krivine and to support on-the-fly extensions by new instructions with their evaluation rules.

Dependencies (2)

  1. coq >= "8.9.1" & < "8.10~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None