Lutz Strassburger

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.

Grants

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

Cut Elimination in Nested Sequents for Intuitionistic Modal Logics
Pdf        January 7, 2013
To appear 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 (15 pages, accepted for publication in APAL)    July 31, 2012

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
Habilitatation à 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")
To appear in Mathematical Structures in Computer Science

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")
To appear in ACM ToCL

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

What is the Problem with Proof Nets for Classical Logic ?
Pdf       April 6, 2010
(to appear 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. We are working on a corrected version.

Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
Pdf (15 pages)    April 10, 2009 (to appear in proceedings of TLCA'09)
Submitted version with 24 pages apendix    January 5, 2009

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

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

Publications