Logical Approaches to Computational Barriers

LJQ: A Strongly Focused Calculus for Intuitionistic Logic

Speaker:
| Roy Dyckhoff |

Author(s): |
Roy Dyckhoff and Stéphane Lengrand |

LJQ is a focused sequent calculus (due to Herbelin) 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.

websites: Arnold Beckmann | 2006-06-23 |