Computability in Europe 2006
Logical Approaches to Computational Barriers
Special Session Talk:
|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|