Lutz Strassburger

ESSLLI'25: I am giving a course (joint with Victoria Barrett) "A gentle introduction to deep inference" (course webpage).
6th Proof Society International School and Workshop, University of Birmingham, UK, 9-13 September 2024.
Dagstuhl seminar 24341: Proof Representations: From Theory to Applications, Schloss Dagstuhl, Germany, 18--23 August 2024.
Logic at the Interface: Modal Logic and AI, University of Montpellier, France, 11--12 July 2024.
9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Tallinn, Estonia, on 10-13 July 2024.
Thirty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) Tallinn, Estonia, 8-11 July 2024
TABLEAUX 2023: 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, September 18-21, 2023, Prague, Czech Republic.
ESSLLI'23 July 31 to August 11, 2023, University of Ljubljana, Slovenia
CSL'23: Computer Science Logic 2023, Annual conference of the European Association for Computer Science Logic (EACSL), February 13-16, 2023, University of Warsaw, Poland
ESSLLI'22: I am giving a course (joint with Sonia Marin) "From Axioms to Rules — The Factory of Modal Proof Systemsrial Proofs" (course webpage).
IJCAR 2022: International Joint Conference on Automated Reasoning 2022, August 7-12, Haifa, Israel (part of FLoC 2022)
Logic and transdiciplinarity: Mathematics/Computer Science/ Philosophy/Linguistics: 7-11 February 2022 CIRM, Marseille, France. Part of thematic month "Logic and Interactions"
TABLEAUX 2021: 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, 6-9 September 2021, Birmingham, UK
ESSLLI'21: I am giving a course (joint with Willem Heijltjes) "From Proof Nets to Combinatorial Proofs — A new approach to Hilbert's 24th problem" (course webpage).
5th International Workshop on Trends in Linear Logic and Applications TLLA 2021, Online (Rome virtually), 27-28 June 2021, Affiliated with LICS 2021
Sixth TICAMORE Meeting (Translating and Discovering Calculi for Modal and Related Logics), Marseille, 5-6 October 2020
ESSLLI'19: I am giving a course (joint with Andrea Aler Tubella) "An introduction to deep inference" (course webpage).
3rd FISP Meeting, TU Wien, December 7-8, 2018

Workshop: Twenty Years of Deep Inference, Oxford, July 2018, part of FLoC 2018
ESSLLI'17: I gave a course (joint with Roman Kuznets) on "Efficient Proof Systems for Modal Logics" (course webpage).
Second FISP Meeting, 8-10 June 2017 in Paris
Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science(LICS) July 5–8, 2016, New York City, USA
Workshop on Efficient and Natural Proof Systems (WENSP) University of Bath 14-16 December, 2015
18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS) April 11-19, 2015
Workshop "Structures and Deduction 2014" as part of the Vienna Summer of Logic 2014, July 12th, 2014
LIX Colloquium 2013: The Theory and Application of Formal Proofs November 5-7, 2013
Journées LAC - GeoCal November 24-25, 2011
First STRUCTURAL meeting June 15-17, 2011
Third REDO meeting September 14-16, 2010
ESSLLI'10: I gave a course "Introduction to Proof Theory". (Here are the lecture notes.)
Second REDO meeting November 16-18, 2009
ESSLLI'09: Workshop "Structures and Deduction 2009" in Bordeaux, July 20-24, 2009.
First REDO meeting May 26-29, 2009
Workshop on Structural Proof Theory in Paris, November 19-21, 2008.
Deep Inference Christmas Meeting 2007 in Dresden, December 19, 2007.
Small Workshop on "Theory and Application of Deep Inference", June 21, 2007.
Small Workshop on "The Realm of Cut Elimination", May 14, 2007.
ESSLLI'06: I gave a course on "Proof Nets and the Identity of Proofs". There are lecture notes.
Geocal'06: I coorganized (with Dale Miller) a workshop on Logic Programming and Concurrency.

COMPRONOM—Combinatorial Proof Normalization (Inria Équipe Associée) 2020–2022
FISP—The Fine Structure of Formal Proof Systems and their Computational Interpretations (ANR-Blanc International), 2016-2018
Analytic Calculi for Modal Logics (PHC Amadeus with Theory and Logic Group, Technische Universität Wien), 2016-2017
From Proofs to Counterexamples for Programming (PHC Procope with University of Bonn, Institute for Computer Science), 2012-2013
Extending the Realm of the Curry-Howard-Correspondence (PHC Germaine De Stael with IAM, Universität Bern), 2011-2012
STRUCTURAL—Structural and Computational Proof Theory (ANR-Blanc International), 2011-2013
REDO—Redesigning Logical Syntax (INRIA ARC 2009), 2009-2010
INFER—Theory and Application of Deep Inference (ANR-Blanc), 2007-2010
Deep Inference and the Essence of Proofs (PAI Germaine De Stael with IAM, Universität Bern), 2007-2008
The Realm of Cut Elimination (PAI Amadeus with Theory and Logic Group, Technische Universität Wien), 2007-2008
(there will be a workshop on May 14, 2007, related to this project)

Publications

List in the dblp computer science bibliography
List on Google Scholar

Intuitionistic S4 is decidable
with Marianna Girlando, Roman Kuznets, Sonia Marin, and Marianela Morales
Pdf    May 2023
To be presented at LICS 2023, Boston, US, June 26-29, 2023

Coqlex: Generating Formally Verified Lexers
with Wendlasida Ouedraogo and Gabriel Scherer
Pdf    May 2023
To appear in The Art, Science, and Engineering of Programming

A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
with Lê Thành Dũng Nguyễn
Pdf    September 2022
(long version of "BV and Pomset Logic are not the same")

Combinatorial Flows as Bicolored Atomic Flows
with Giti Omidvar
Pdf        September 2022
Presented at WoLLIC 2022

Normalization without syntax
with Willem Heijltjes and Dominic Hughes
Pdf        August 2022
In proceedings of FSCD 2022

A Graphical Proof Theory of Logical Time
with Matteo Acclavio, Ross Horne and Sjouke Mauw
Pdf        August 2022
In proceedings of FSCD 2022

BV and Pomset Logic are not the same
with Lê Thành Dũng Nguyễn
Pdf    October 2021
Proceedings of CSL 2022.

Justification logic for constructive modal logic
with Roman Kuznets and Sonia Marin
Pdf of IMLA 2017     (August 2017)
Pdf of Journal of Applied Logics - IfCoLog Journal 8(8):p.2313-2332    (September 2021)

Game Semantics for Constructive Modal Logic
with Matteo Acclavio and Davide Catta
Pdf    September 2021
Proceedings of TABLEAUX 2021.

Combinatorial Proofs and Decomposition Theorems for First-order Logic
with Dominic Hughes and Jui-Hsuan Wu
Pdf        April 2021
Proceedings of LICS 2021

A fully labelled proof system for intuitionistic modal logics
with Sonia Marin and Marianela Morales
Pdf     October 2020
Journal of Logic and Computation

MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
with Marianna Girlando
Pdf    June 2020
Proceedings of IJCAR 2020 (Springer Link)

Logic beyond formulas: a proof system on graphs
with Matteo Acclavio and Ross Horne
Pdf (short version for proceedings)      Pdf (long version with appendix with proofs)      June 2020
In proceedings of LICS 2020

On Combinatorial Proofs for Modal Logic
with Matteo Acclavio
Pdf    September 2019
Proceedings of TABLEAUX 2019.

Towards a Combinatorial Proof Theory
with Benjamin Ralph
Pdf    September 2019
Proceedings of TABLEAUX 2019.

On Combinatorial Proofs for Logics of Relevance and Entailment
with Matteo Acclavio
Pdf    April 2019
Proceedings of WoLLIC 2019.

Intuitionistic proofs without syntax
with Willem Heijltjes and Dominic Hughes
Pdf        June 2019
In proceedings of LICS 2019

Proof nets for first-order additive linear logic
with Willem Heijltjes and Dominic Hughes
Pdf        June 2019
In proceedings of FSCD 2019
longer version (September 4, 2018) available as Inria research report RR-9201

On the Decision Problem for MELL
Pdf        February 19, 2019
Theoretical Computer Science, Volume 768, Pages 91-98        (freely downloadable from Elsevier until May 11, 2019)
also available as Inria RR-9203 (Pdf, September 7, 2018)

The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
Pdf        November 16, 2018
Philosophical Transactions of the Royal Society, Volume 377, Issue 2140

Deep Inference and Expansion Trees for Second Order Multiplicative Linear Logic
Pdf        September 7, 2018
Mathematical Structures in Computer Science

From Syntactic Proofs to Combinatorial Proofs
with Matteo Acclavio
Pdf    April 20, 2018
Proceedings of IJCAR 2018.

Maehara-style modal nested calculi
with Roman Kuznets
Pdf    July 18, 2018
Archive for Mathematical Logic, 1-27 2018.

Proof Theory for Indexed Nested Sequents
with Sonia Marin
Pdf    July 7, 2017
Proceedings of TABLEAUX 2017.
There is also a technical report with more details (Pdf)

Combinatorial Flows and Their Normalisation
Pdf    August 19, 2017
Proceedings of FSCD 2017.
The Inria research report "Combinatorial Flows and Proof Compression" listed below contains more details.

Combinatorial Flows and Proof Compression
Pdf    March 30, 2017
Inria Research Report RR-9048.

On the Length of Medial-Switch-Mix Derivations
with Paola Bruscoli
Pdf    May 22, 2017
Proceedings of WoLLIC 2017.

Non-Crossing Tree Realizations of Ordered Degree Sequences
with Laurent Méhats
Pdf        ©Springer-Verlag           December 6, 2016
Proceedings of LACLS 2016
There is also a technical report with full proofs.

Modular Focused Proof Systems for Intuitionistic Modal Logics
with Sonia Marin and Kaustuv Chaudhuri
Pdf    May 1, 2016
To appear in proceedings of FSCD 2016.

Focused and Synthetic Nested Sequents
with Sonia Marin and Kaustuv Chaudhuri
Pdf        ©Springer-Verlag           January 6, 2016
Proceedings of FoSSaCS 2016 (The official proceedings version is full of mistakes introduced by Springer's "copyeditors" and we strongly recommend reading the authors' versions instead.)
There is also a technical report with full proofs.

No complete linear term rewriting system for propositional logic
with Anupam Das
Pdf        April 26, 2015
Proceedings of RTA 2015

On the Power of Substitution in the Calculus of Structures
with Novak Novaković
Pdf        November 24, 2014
ACM ToCL 16(3:19), 2015

Parametricity and Proving Free Theorems for Functional-Logic Languages
with Stefan Mehner, Daniel Seidel, and Janis Voigtländer
Pdf        August 24, 2014
In proceedings of PPDP 2014

Label-free Modular Systems for Classical and Intuitionistic Modal Logics
with Sonia Marin
Pdf        June 6, 2014
AiML 2014

Proof nets and semi-⋆-autonomous categories
with Willem Heijltjes
Pdf        May 9, 2014
Mathematical Structures in Computer Science

On Nested Sequents for Constructive Modal Logics
with Ryuta Arisaka and Anupam Das
Pdf        May 17, 2014
LMCS 11 (3:7) 2015

Symmetric Normalisation for Intuitionistic Logic
with Nicolas Guenot
Pdf        May 15, 2014
In proceedings of CSL-LICS 2014.

Herbrand Confluence
with Stefan Hetzl
Pdf        December, 2013
Logical Methods in Computer Science 9(4) (2013)

A logical basis for quantum evolution and entanglement
with Richard F. Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden
Pdf        July 18, 2013
Categories and Types in Logic, Language, and Physics --- Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday

Cut Elimination in Nested Sequents for Intuitionistic Modal Logics
Pdf        January 7, 2013
In proceedings of FoSSaCS 2013

Herbrand-Confluence for Cut Elimination in Classical First Order Logic
with Stefan Hetzl
Pdf        June 22, 2012
Appeared in proceedings of CSL'12

Extension without Cut
Pdf    July 31, 2012
Annals of Pure and Applied Logic Volume 163, Issue 12, December 2012, Pages 1995-2007

The Focused Calculus of Structures
with Nicolas Guenot and Kaustuv Chaudhuri
Pdf        June 22, 2011
To appear in proceedings of CSL'11

Towards a Theory of Proofs of Classical Logic
Pdf        December 3, 2010
Habilitation à diriger des recherches
Defense: January 7, 2011

A System of Interaction and Structure V: The Exponentials and Splitting
with Alessio Guglielmi
Pdf       December 3, 2010
(second part of the long version of "A Non-commutative Extension of MELL")
Mathematical Structures in Computer Science, 21(3), pp.563-584, 2011

A System of Interaction and Structure IV: The Exponentials and Decomposition
with Alessio Guglielmi
Pdf    (also available from http://arxiv.org/abs/0903.5259)     July 27, 2010
(first part of the long version of "A Non-commutative Extension of MELL" in LPAR 2002)
ACM ToCL 12(4:23), 2011

Breaking Paths in Atomic Flows for Classical Logic
with Alessio Guglielmi and Tom Gundersen
Pdf       April 29, 2010
In proceedings of LICS'10

What is the Problem with Proof Nets for Classical Logic ?
Pdf       April 6, 2010
In proceedings of CiE'10

From Deep Inference to Proof Nets via Cut Elimination
Pdf (preprint)        June 24, 2009
Journal of Logic and Computation 2009; doi: 10.1093/logcom/exp047
Abstract (from the JLC webpage)
Pdf (from the JLC webpage)
(This is the Journal version of "From Deep Inference to Proof Nets" presented at SD'05)

Expanding the realm of systematic proof theory
with Agata Ciabattoni and Kazushige Terui
Pdf       June 22, 2009
(to appear in proceedings of CSL'09)

Modular sequent systems for modal logic
with Kai Brünnler
proceedings of Tableaux 2009, LNCS 5607, pp. 152-166
Attention: This paper contains some serious mistakes. The paper "Label-free Modular Systems for Classical and Intuitionistic Modal Logics" (with Sonia Marin) in AiML 2014 gives more details.

Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
Pdf (15 pages),    April 10, 2009
In proceedings of TLCA'09

A Kleene Theorem for Forest Languages
Pdf (12 pages),    December 17, 2008
In proceedings of LATA'09

The Logic BV and Quantum Causality
with Rick Blute and Prakash Panangaden
Pdf (2 pages)    September 12, 2008
Presented at Trends in Logic VI: Logic and the foundations of physics: space, time and quanta

Deep Inference for Hybrid Logic
Pdf (10 pages, accepted at HyLo'07)    May 15, 2007

A Characterisation of Medial as Rewriting Rule
Pdf (15 pages, accepted at RTA'07)    February 2, 2007
BibTeX entry

Proof Nets and the Identity of Proofs
Lecture notes for the course given at ESSLLI'06.
Pdf (Handout version)    June 27, 2006
Pdf (INRIA Research Report, also available from https://hal.inria.fr/inria-00107260 and http://arxiv.org/abs/cs.LO/0610123)
November 2006
BibTeX entry

What could a Boolean category be?
Pdf    June 21, 2006
Short version of "On the Axiomatisation of Boolean Categories with and without Medial".
Presented at Cl&C'06 (Satellite Workshop of ICALP'06).

On the Axiomatisation of Boolean Categories with and without Medial
Pdf    June, 2007
Appeared in Theory and Applications of Categories, Vol. 18, 2007, No. 18, pp 536-601.

From Proof Nets to the Free *-Autonomous Category
with François Lamarche
Journal version of "On Proof Nets for Multiplicative Linear Logic with Units" (see below)
Appeared in Logical Methods in Computer Science, Vol 2 (4:3), pp. 1-44.
Pdf    October 5, 2006    (also available from http://arxiv.org/abs/cs.LO/0605054)
BibTeX entry

From Deep Inference to Proof Nets
Pdf        June 16, 2005
Presented at SD'05 (Satellite Workshop of ICALP'05).

What is a logic, and what is a proof ?
Pdf     October 23, 2006
(version for second edition of Logica Universalis, pp. 135-152, ©Birkhäuser)
BibTeX entry

Constructing free Boolean Categories
with François Lamarche
Pdf    (Final version for proceedings)    April 8, 2005
LICS'05
Pdf    (Version with complete proofs)    February 18, 2005

Naming Proofs in Classical Propositional Logic
with François Lamarche
Pdf        ©Springer-Verlag        January 31, 2005
TLCA'05, LNCS 3461, pp. 246-261      BibTeX entry

On Proof Nets for Multiplicative Linear Logic with Units
with François Lamarche
Pdf        ©Springer-Verlag        June 30, 2004
CSL 2004, LNCS 3210, pp. 145-159      BibTeX entry

System NEL is Undecidable
Pdf        August 1, 2003
WoLLIC 2003, Electronic Notes in Theoretical Computer Science 84        BibTeX entry

Linear Logic and Noncommutativity in the Calculus of Structures
Pdf       Pdf in booklet format        July 25, 2003
PhD thesis, successfully defended on July 24, 2003      BibTeX entry

A Non-commutative Extension of Multiplicative Exponential Linear Logic
with Alessio Guglielmi
Technical Report WV-02-03, TU Dresden
(Now obsolete and replaced by "A System of Interaction and Structure IV: The Exponentials and Decomposition" and "A System of Interaction and Structure V: The Exponentials and Splitting")
A Non-commutative Extension of MELL
with Alessio Guglielmi
Pdf        © Springer-Verlag        August 9, 2002
LPAR 2002, LNAI 2514, pp. 231-246      BibTeX entry

A Local System for Linear Logic
Pdf        © Springer-Verlag        August 9, 2002
LPAR 2002, LNAI 2514, pp. 388-402        BibTeX entry

MELL in the Calculus of Structures
Pdf        October 29, 2001
Theoretical Computer Science, Vol. 309, pp. 213-285     BibTeX entry

Non-commutativity and MELL in the Calculus of Structures
with Alessio Guglielmi
Pdf        © Springer-Verlag        June 28, 2001
CSL 2001, LNCS 2142, pp. 54-68      BibTeX entry

Rational Forest Languages and Sequential Forest Transducers
PostScript      PostScript in booklet format
April 6, 2000
Master's thesis, successfully defended on April 25, 2000      BibTeX entry

Lutz Straßburger

Lutz Straßburger

Current Position:

Research

Events

Grants

Software

Publications