Lutz Straßburger
Current Position:
Research scientist (in French: chargé
de recherche, CR1) at INRIA Research Centre Saclay - Île-de-France
within the Parsifal
team.
Postal Address:
École Polytechnique
Laboratoire d'Informatique
(LIX)
Projet Parsifal
Rue de Saclay
91128 Palaiseau Cedex
France
Office: 412-24
Telephone: +33 (0)1 69 33 40 68
Fax: +33 (0)1 69 33 40 49
Email: lutz AT lix DOT polytechnique DOT fr
Research
Events
- ESSLLI'10:
I will give a course "Introduction to Proof Theory".
- 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
Papers
Extension without Cut
Pdf (17 pages)
August 20, 2009
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
Pdf
February 2, 2009
(to appear in proceedings of TABLEAUX'09)
A System of Interaction and Structure IV: The Exponentials and Decomposition
with Alessio
Guglielmi
Pdf
March 29, 2009
(first part of the long version of "A Non-commutative Extension of MELL")
A System of Interaction and Structure V: The Exponentials and Splitting
with Alessio
Guglielmi
Pdf
March 29, 2009
(second part of the long version of "A Non-commutative Extension of MELL")
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
Last update:
March 29, 2009
Lutz
Straßburger