LJQ: a strongly focused calculus for intuitionistic logic

Roy Dyckhoff, Stéphane Lengrand

Research output: Chapter in Book/Report/Conference proceedingConference contribution

27 Citations (Scopus)


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 languageEnglish
Title of host publicationLecture Notes in Computer Science
Number of pages13
ISBN (Print)978-3-540-35466-6
Publication statusPublished - Jul 2006


Dive into the research topics of 'LJQ: a strongly focused calculus for intuitionistic logic'. Together they form a unique fingerprint.

Cite this