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)

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

Fingerprint

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

Cite this