# Contribution: ClassicalRealizability

Krivine's classical realizability

## Authors

- Lionel Rieg

## 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.

## Keywords

classical realizability, krivine's realizability, primitive datatype, non determinism, quote, axiom of countable choice, real numbers

## README

Copyright (c) 2014, Lionel Rieg DESCRIPTION =========== The aim of the library is to provide a framework for checking proofs in Krivine's classical realizability. As the original theory by Krivine, it is very modular and supports extension of the KAM by new instructions and their evaluation rules on the fly. The main limitation of this library is that it currently only admits to use one pole at a time. In particular, any proof using more than one pole (like the absence of a univesal realizer of the recurrence axiom under a deterministic evaluation) cannot be directly expressed. The library is structured as follows: + A core component gathered in Kbase.v: - ShallowEmbedding.v: basic definition of the KAM and Krivine's realizability - Tactics.v: automatization tactics to ease proofs - BasicResults.v: elementary results in calssical realizability - Subtyping.v: subtyping between formulĂ¦ which permits simpler reasoning - PropEmbedding.v: a translation of Prop into realizability formulĂ¦ + Several extensions of the core theory: - SimpleExtensions.v: easy extensions by adding new instructions - Peano.v: realization of Peano arithmetic - KBool.v: description, properties and specification of booleans - Fork.v: description, properties and specification of non-determinism - Quote.v: the 'quote' instruction, with the realizer of the countable AC - Dedekind: partial formalization of real numbers by Dedekind cuts - Integers.v: native integers - Rationals.v: native rational numbers + A partial formalization of real numbers by (a variant of) Cauchy sequences, gatherd in Reals.v: - QcOrderedType.v, QcComplement.v, Qcminmax.v, Qcabs.v: auxiliary results about the QCanon type, including a definition of absolute value - Real_defintions.v: basic definition of reals numbers - Real_relations.v: comparisons on real numbers and their properties - Real_operations.v: operations on real numbers and their properties - Real_axioms.v: Axioms of real numbers BUILDING ======== Simply type compile all the files with: make If it does not work, you can easily regenerate the makefile with the following command: coq_makefile *.v -o makefile It is known to compile with Coq v.8.4pl3. To generate the documentation in an existing directiry "doc/", type coqdoc --utf8 -g -d doc/ *.v LICENCE ======= This library is available under the CeCILL-B licence.

## Available files

- ClassicalRealizability.Real_relations.html
- ClassicalRealizability.Reals.html
- ClassicalRealizability.Kbase.html
- ClassicalRealizability.BasicResults.html
- ClassicalRealizability.ShallowEmbedding.html
- ClassicalRealizability.Real_operations.html
- ClassicalRealizability.Peano.html
- ClassicalRealizability.Qccomplement.html
- ClassicalRealizability.LogicalEquivalences.html
- ClassicalRealizability.Real_axioms.html
- ClassicalRealizability.Real_definitions.html
- ClassicalRealizability.QcOrderedType.html
- ClassicalRealizability.Subtyping.html
- ClassicalRealizability.Rationals.html
- ClassicalRealizability.Qcabs.html
- ClassicalRealizability.Integers.html
- ClassicalRealizability.Dedekind.html
- ClassicalRealizability.Fork.html
- ClassicalRealizability.Qcminmax.html
- ClassicalRealizability.Tactics.html
- ClassicalRealizability.PropEmbedding.html
- ClassicalRealizability.SimpleExtensions.html
- ClassicalRealizability.Quote.html
- ClassicalRealizability.KBool.html