Program Extraction from Classical Proofs

15 years 10 months ago

Download www.brics.dk

We demonstrate program extraction by the Light Dialectica Interpretation (LDI) on a minimal logic proof of the classical existence of Fibonacci numbers. This semi-classical proof is available in MinLog's library of examples. The term of G

Ulrich Berger, Helmut Schwichtenberg

Real-time Traffic

Algorithms | Dialectica Interpretation | Fibonacci Numbers | LCC 1994 | Light Dialectica |

claim paper

» Relating Classical Realizability and Negative Translation for Existential Witness Extracti...

» Understanding and Using Spectors Bar Recursive Interpretation of Classical Analysis

» Program Extraction from Normalization Proofs

» Uniform Heyting arithmetic

» Existential witness extraction in classical realizability and via a negative translation

» Classical Program Extraction in the Calculus of Constructions

» Program Extraction From Proofs of Weak Head Normalization

» Extracting Computer Algebra Programs from Statements

Post Info
More Details (n/a)

Added	10 Aug 2010
Updated	10 Aug 2010
Type	Conference
Year	1994
Where	LCC
Authors	Ulrich Berger, Helmut Schwichtenberg

Comments (0)

Sciweavers

Program Extraction from Classical Proofs

Algorithms | Dialectica Interpretation | Fibonacci Numbers | LCC 1994 | Light Dialectica |

Explore & Download

Productivity Tools

Sciweavers