Title: LJQ, a Strongly Focused Calculus for Intuitionistic Logic

Type: Book Section

Citation:

Dyckhoff, R, Lengrand, S. In: Lecture Notes in Computer Science 3988, Beckmann, A, Berger, U, Löwe, B, Tucker, JV (eds), Proc. 2nd Conference on Computability in Europe (CiE'06): Logical Approaches to Computational Barriers, pp 173-185. Springer-Verlag. 2006.

Abstract:

LJQ is a focused sequent calculus for intuitionistic logic, with a simple restriction on the first premiss 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.

BibTeX:

@incollection{DyckRLengS2006,
volume = {3988},
location = {Swansea, UK},
pdf = {http://www.cs.st-andrews.ac.uk/~rd/publications/cie2006.pdf},
author = {Roy Dyckhoff and St\'ephane Lengrand},
series = {Lecture Notes in Computer Science},
booktitle = {Logical Approaches to Computational Barriers: Proc. 2nd Conference on Computability in Europe, CiE 2006},
editor = {Arnold Beckmann and Ulrich Berger and Benedikt L{\"o}we and John V. Tucker},
url = {http://www.cs.st-andrews.ac.uk/research/publications/DL06.php},
title = {LJQ, a Strongly Focused Calculus for Intuitionistic Logic},
publisher = {Springer-Verlag},
pages = {173-185},
year = {2006},
bibsource = {http://www-fp.cs.st-andrews.ac.uk/bib.shtml?2006}
}

Download:

• PDF