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.10.0.tar.gz
md5=988099e8c3d1b7110aa0faf0a2a21128
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