Institut Mittag-Leffler
The Royal Swedish Academy of Sciences


Reports Institut Mittag-Leffler
ISSN: 1103-467X
ISRN: IML-R


Refined Program Extraction from Classical Proofs
Source file as TeX DVI Data Postscript Document Portable Document Format

Ulrich Berger , Wilfried Buchholz , Helmut Schwichtenberg

Preprint series: Mathematical Logic - 2000/2001, No. 14

MSC 2000

03F10 Functionals in proof theory
03F50 Metamathematics of constructive systems

Keywords: Program extraction, A-translation, Definite formula