| 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 |
