Computability in Europe 2006
Logical Approaches to Computational Barriers

Special Session Talk:
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