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

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