Name
Abstract | ||
|---|---|---|
. Recently there has been much interest in the problem of findingthe computational content of classical reasoning. One of the most appealingdirections for the computer scientist to tackle such a problem is the relationwhich has been established between classical logic and lambda calculi withcontrol operators, like Felleisen's control operator C. In this paper we introducea typed lambda calculus with the C operator corresponding to PeanoArithmetic, and a set of reduction rules related to... |
Year | DOI | Venue |
|---|---|---|
1993 | 10.1007/BFb0037097 | TLCA |
Keywords | Field | DocType |
classical logic,control-like reductions,extracting constructive content,typed lambda calculus | Peano axioms,Algebra,Simply typed lambda calculus,Typed lambda calculus,Computer science,Natural deduction,System F,Minimal logic,Algorithm,Pure type system,Curry–Howard correspondence | Conference |
ISBN | Citations | PageRank |
3-540-56517-5 | 25 | 2.51 |
References | Authors | |
8 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Franco Barbanera | 1 | 357 | 35.14 |
| Stefano Berardi | 2 | 373 | 51.58 |