LJQ: a strongly focused calculus for intuitionistic logic

Roy Dyckhoff; Stéphane Lengrand

doi:10.1007/11780342_19

LJQ: a strongly focused calculus for intuitionistic logic

Roy Dyckhoff, Stéphane Lengrand

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

LJQ is a focused sequent calculus 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.

Original language	English
Title of host publication	Lecture Notes in Computer Science
Publisher	Springer-Verlag
Pages	173-185
Number of pages	13
Volume	3988
ISBN (Print)	978-3-540-35466-6
DOIs	https://doi.org/10.1007/11780342_19
Publication status	Published - Jul 2006

Access to Document

10.1007/11780342_19

Cite this

@inproceedings{c5587a7babee4619bcf6e98a73cd4940,

title = "LJQ: a strongly focused calculus for intuitionistic logic",

abstract = "LJQ is a focused sequent calculus 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.",

author = "Roy Dyckhoff and St{\'e}phane Lengrand",

note = "Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, Lecture Notes in Computer Science (eds A. Beckmann et al)",

year = "2006",

month = jul,

doi = "10.1007/11780342_19",

language = "English",

isbn = "978-3-540-35466-6",

volume = "3988",

pages = "173--185",

booktitle = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag",

address = "Germany",

}

TY - GEN

T1 - LJQ: a strongly focused calculus for intuitionistic logic

AU - Dyckhoff, Roy

AU - Lengrand, Stéphane

N1 - Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, Lecture Notes in Computer Science (eds A. Beckmann et al)

PY - 2006/7

Y1 - 2006/7

N2 - LJQ is a focused sequent calculus 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.

AB - LJQ is a focused sequent calculus 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.

UR - http://www.springerlink.com/(uf50w345bcthn455xs0hzqvz)/app/home/contribution.asp?referrer=parent&backto=issue,19,61;journal,56,3904;linkingpublicationresults,1:105633,1

U2 - 10.1007/11780342_19

DO - 10.1007/11780342_19

M3 - Conference contribution

SN - 978-3-540-35466-6

VL - 3988

SP - 173

EP - 185

BT - Lecture Notes in Computer Science

PB - Springer-Verlag

ER -

LJQ: a strongly focused calculus for intuitionistic logic

Abstract

Access to Document

Other files and links

Fingerprint

Cite this