Head of the Partout team.

Inria Saclay - Île-de-France

1 rue Honoré d'Estienne d'Orves

Bâtiment Alan Turing

Campus de l'École Polytechnique

91120 Palaiseau

France

theoretical computer science,

proof theory and its applications, in particular, logic programming, functional programming, and software verification,

proof complexity,

deep inference,

category theory

proof theory and its applications, in particular, logic programming, functional programming, and software verification,

proof complexity,

deep inference,

category theory

- 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)

- MOIN: a prover for modal and intuitionistic nested sequents

- List in the dblp computer science bibliography
- List on Google Scholar

A fully labelled proof system for intuitionistic modal logics

with Sonia Marin and Marianela Morales

Pdf October 2020

Submitted

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

Last update: October 26, 2020 Lutz Straßburger