Name
Abstract | ||
|---|---|---|
LJQ is a focused sequent calculus for intuitionistic logic, with a simple restriction on the first premisss of the usual left introduction rule for implication. We discuss its history (going back to about 1950, or beyond), present the underlying theory and its applications both to terminating proof-search calculi and to call-by-value reduction in lambda calculus. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11780342_19 | CiE |
Keywords | Field | DocType |
simple restriction,focused sequent calculus,lambda calculus,intuitionistic logic,underlying theory,usual left introduction rule,proof-search calculus,sequent calculus | Discrete mathematics,Typed lambda calculus,Natural deduction,Computer science,Minimal logic,Proof calculus,Noncommutative logic,Many-valued logic,Cut-elimination theorem,Calculus,Curry–Howard correspondence | Conference |
Volume | ISSN | ISBN |
3988 | 0302-9743 | 3-540-35466-2 |
Citations | PageRank | References |
22 | 1.28 | 14 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Roy Dyckhoff | 1 | 452 | 49.09 |
| Stéphane Lengrand | 2 | 162 | 11.43 |