Title | Getting results from programs extracted from classical proofs |
Author(s) | Christophe Raffalli |
Type | Article in Journal |
Abstract | We 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. |
Length | 20 |
Copyright | Copyright © 2004 Elsevier B.V. All rights reserved. |
File |
|
URL |
http://dx.doi.org/10.1016/j.tcs.2004.03.006 |
Language | English |
Journal | Theoretical Computer Science |
Volume | 323, Issues 1-3 |
Pages | 49-70 |
Year | 2004 |
Month | September |
Edition | 0 |
Translation |
No |
Refereed |
Yes |