package coq-classical-realizability
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Krivine's classical realizability
Install
Dune Dependency
Authors
Maintainers
Sources
v8.5.0.tar.gz
md5=7e6fb42bd18a9d7282d8d694d322f9a6
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.
On This Page