Computability in Europe 2006
Logical Approaches to Computational Barriers
Logical Approaches to Computational Barriers
Print this page
Special Session Talk:
LJQ: A Strongly Focused Calculus for Intuitionistic Logic
| Speaker: | Roy Dyckhoff |
| Author(s): | Roy Dyckhoff and Stéphane Lengrand |
| Presentation: | Dyckhoff-Lengrand.pdf |
Abstract
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
|