Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

12

MLQ
1998

favoriteEmaildiscussreport

61views more MLQ 1998»

Extracting Algorithms from Intuitionistic Proofs

13 years 4 months ago

Extracting Algorithms from Intuitionistic Proofs

Download www.ciul.ul.pt

This paper presents a new method – which does not rely on the cut-elimination theorem – for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an inﬁnitary language. We illustrate the method for the intuitionistic counterpart of Buss’s theory S1 2 , and we brieﬂy sketch it for the other levels of bounded

Fernando Ferreira, António Marques

Real-time Traffic

Certain Intuitionistic Subsystems | Intuitionistic Counterpart | MLQ 1998 | Realizability Argument |

claim paper

Related Content

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

» On Transforming Intuitionistic Matrix Proofs into StandardSequent Proofs

» Proof Search and CounterModel Construction for Biintuitionistic Propositional Logic with L...

» Program Extraction from Normalization Proofs

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

» Program Extraction from Classical Proofs

» Program Extraction from Large Proof Developments

» Program Extraction From Proofs of Weak Head Normalization

» Extracting a Normalization Algorithm in IsabelleHOL

Post Info
More Details (n/a)

Added	22 Dec 2010
Updated	22 Dec 2010
Type	Journal
Year	1998
Where	MLQ
Authors	Fernando Ferreira, António Marques

Comments (0)