Olivier Laurent (LIP, ENS Lyon), Around classical and intuitionistic linear logics

Schedule

Abstract

We revisit the syntactic relations between classical linear logic (LL) and intuitionistic linear logic (ILL). This includes a study of double-negation translations from LL to ILL and a new conservativity result for LL over ILL. Applying these results to LL and tensor logic (the “positive” fragment of ILL) allows us to show how the “at most one positive formula” property of focused systems for LL can be seen as a particular case of the “at most one right-hand side formula” property of intuitionistic systems.