Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal

Details:

   
TitleGetting results from programs extracted from classical proofs
Author(s) Christophe Raffalli
TypeArticle in Journal
AbstractWe present a new method to extract from a classical proof of for all x (I[x] → there exists y (O[y] and S[x,y])) a program computing y from x. This method applies when O is a data type and S is a decidable predicate. Algorithms extracted this way are often far better than a stupid enumeration of all the possible outputs and this is verified on a nontrivial example: a proof of Dickson's lemma.
Length20
CopyrightCopyright 2004 Elsevier B.V. All rights reserved.
File
URL http://dx.doi.org/10.1016/j.tcs.2004.03.006
LanguageEnglish
JournalTheoretical Computer Science
Volume323, Issues 1-3
Pages49-70
Year2004
MonthSeptember
Edition0
Translation No
Refereed Yes
Webmaster