Program Extraction from Classical Proofs

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

• Type: Conference
• Year: 1994
• Where: LCC
• Authors: Ulrich Berger, Helmut Schwichtenberg
• Keywords: Algorithms, Dialectica Interpretation, Fibonacci Numbers, LCC 1994, Light Dialectica