Research

This list includes research articles as well as unpublished notes on my various research interests: Rewriting theory, Proof theory & Games semantics, Categorical algebra and Type theory & Realizability.

Rewriting Theory

Explicit substitutions and strong normalization

Typed lambda-calculi with explicit substitutions may not terminate
Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, Edinburgh,
Lecture Notes in Computer Science 902, pp. 328-334, Springer, 1995.
TLCA'95
PostScript (7 pages)

Four typed lambda-calculi with explicit substitutions may not terminate: the first examples
Manuscript, Paris, April 1994.
PostScript (5 pages)

On a duality between Kruskal and Dershowitz theorems
Proceedings of the 25th International Colloquium on Automata Languages and Programming, Aalborg, 1998.

ICALP'98
Pdf (12 pages)

Coherence in braided monoidal categories

Braids as a conflict-free rewriting system
Manuscript, Amsterdam, 1995.
PostScript (12 pages)

MacLane's coherence theorem viewed as a word problem.
Prépublication de l'équipe PPS (October 2003, number 25).
Manuscript, Paris, 2000.
PostScript (10 pages)

Axiomatic Rewriting Theory

An abstract standardisation theorem
with Georges Gonthier and Jean-Jacques Lévy,
Proceedings of the 7th Annual Symposium on Logic in Computer Science, Santa Cruz, 1992.
LiCS'92
PostScript (10 pages)

Axiomatic Rewriting Theory I
A diagrammatic standardization theorem
Processes, Terms and Cycles: Steps on the Road to Infinity.
Essays dedicated to Jan Willem Klop on the occasion of his 60th birthday.
Edited by Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk and Roel de Vrijer.
Springer Verlag, Lecture Notes in Computer Science 3838.
Note: a preliminary version appeared as Prépublication de l'équipe PPS (December 2002, number 13).
Pdf (81 pages)

Axiomatic Rewriting Theory II
The lambda-sigma calculus enjoys finite normalisation cones
Journal of Logic and Computation, vol 10 No. 3, pp. 461-487, 2000.
Preliminary version: PostScript (30 pages)

Axiomatic Rewriting Theory III
A factorisation theorem in Rewriting Theory
Proceedings of the 7th Conference on Category Theory and Computer Science, Santa Margherita Ligure,
Lecture Notes in Computer Science 1290, pp. 49-68, Springer, 1997.
CTCS'97
PostScript (20 pages)

Axiomatic Rewriting Theory IV
A stability theorem in Rewriting Theory
Proceedings of the 13th Annual Symposium on Logic in Computer Science, Indianapolis, pp. 287-298, 1998.
LiCS'98
PostScript (12 pages)

Axiomatic Rewriting Theory V
Computations as events
In preparation.

Axiomatic Rewriting Theory VI
Residual theory revisited
Proceedings of Conference on Rewriting Techniques and Applications, Copenhague, 2002.
RTA'02 (Best paper award of the conference.)
PostScript (17 pages)

Axiomatic Rewriting Theory VII
Explicit substitutions without critical pairs
In preparation.

Description Abstraite des Systèmes de Réécriture
Thèse de l'Université Paris 7, december 1996.
abstract cover PostScript (229 pages) cover Pdf (229 pages)

Proof Theory & Games Semantics

Linear logic

Three approaches to congruence
with Sacha Bourgeois-Gironde. Proceedings of the International Wittgenstein Colloquium, Kirchberg am Wechsel, 1997. WITT'97
PostScript (7 pages)

Double categories: a modular model of multiplicative linear logic
Mathematical Structures in Computer Science, vol. 12, pp 449-479, 2002.
Preliminary version: PostScript (31 pages)

A topological correctness criterion for non-commutative logic
Prépublication de l'équipe PPS (December 2002, number 15).
Linear Logic in Computer Science, T. Ehrhard, J-Y. Girard, P. Ruet and P. Scott eds.
London Mathematical Society Lecture Notes Series, Volume 316, 2004.
Preliminary version: PostScript (40 pages)

Games semantics

Concurrent Games and Full Completeness
with Samson Abramsky.
Proceedings of the 15th Annual Symposium on Logic in Computer Science, Trente, 1999.
LiCS'99
PostScript (12 pages)

Categorical models of linear logic revisited
Prépublication de l'équipe PPS (September 2003, number 22).
To appear in Theoretical Computer Science.
Preliminary version: PostScript (37 pages)

Comparing hierarchies of types in models of linear logic
Prépublication de l'équipe PPS (December 2002, number 14).
Information and Computation, Volume 189, Issue 2, Pages 202-234, March 2004.
Preliminary version: PostScript (36 pages) Pdf (36 pages)

Sequential algorithms and strongly stable functions
Full version of Sequentiality and extensionality
(circulated as lecture notes during the LINEAR summer school, the Azores, September 2000.)
Special Issue « Game Theory Meets Theoretical Computer Science » of Theoretical Computer Science Volume 343, Issue 1, Pages 237-281, 2005.
Preliminary version: PostScript (52 pages) Pdf (52 pages)

Resource modalities in game semantics
with Nicolas Tabareau.
Proceedings of the 22nd Conference on Logic in Computer Science, Wroclaw, 2007.
LiCS 2007
Pdf (14 pages)

Resource modalities in tensor logic
with Nicolas Tabareau.
Journal version of the LiCS 2007 paper. Annals in Pure and Applied Logic, Special Issue edited by Dan Ghica and Russ Harmer, Volume 161, Issue 5, Pages 632-653.
APAL 2009
Pdf (35 pages)

An algebraic account of references in game semantics
with Nicolas Tabareau.
Proceedings of the 25th Conference on the Mathematical Foundations of Programming Semantics, Oxford, 2009.
MFPS 2009
Pdf (25 pages)

Asynchronous Games Semantics

Innocence in 2-dimensional games
Unpublished. Notes for the Linear Logic workshop in Copenhagen, January 2002.
PostScript (7 pages)

Asynchronous games 1
A group-theoretic formulation of uniformity
Unpublished. Preliminary version. March 2003.
Pdf (31 pages)

Asynchronous games 2
The true concurrency of innocence
Extended abstract published in the Proceedings of the 15th International Conference on Concurrency Theory, London, 2004.
Lecture Notes in Computer Science 3170, pp. 448-465, Springer Verlag.
Extended Abstract: Pdf (17 pages)
CONCUR 2004
Journal version published in the Special Issue « Selected papers of CONCUR 2004 » of Theoretical Computer Science Volume 358, Issues 2-3, pages 200-228, 2006.
Preliminary journal Version: Pdf (45 pages)

Asynchronous games 3
An innocent model of linear logic
Proceedings of the 10th Conference on Category Theory and Computer Science, Copenhagen, 2004.
CTCS 2004
Pdf (21 pages)

Asynchronous games 4
A fully complete model of propositional linear logic
Proceedings of the 20th Conference on Logic in Computer Science, Chicago, 2005.
LiCS 2005
Pdf (11 pages)

Asynchronous games: innocence without alternation.
with Samuel Mimram,
Proceedings of Concur 2007, Lisboa, 2007.
CONCUR 2007
Pdf (15 pages)

Categorical algebra of proofs and programs

Categorical semantics

Categorical semantics of linear logic
Published in « Interactive models of computation and program behaviour ».
Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine, Paul-André Melliès.
Panoramas et Synthèses 27, Société Mathématique de France, 2009.
Pdf (213 pages)

Functorial boxes in string diagrams
Invited talk at the Computer Science Logic 2006 conference in Szeged, Hungary.
Lecture Notes in Computer Science 4207, Springer Verlag.
Preliminary version: Pdf (43 pages)

An explicit formula for the free exponential modality of linear logic
with Nicolas Tabareau and Christine Tasson.
International Colloquium on Automata, Languages and Programming, Rhodes, Greece, 2009.
Lecture Notes in Computer Science 5556, Springer Verlag.
ICALP 2009
Preliminary version: Pdf (12 pages)
A long version of the paper has been recently submitted to a journal.
The interested reader will find it here.

Categorical combinatorics

Categorical combinatorics for innocent strategies
with Russ Harmer and Martin Hyland.
Proceedings of the 22nd Conference on Logic in Computer Science, Wroclaw, 2007.
LiCS 2007
Pdf (10 pages)

Segal condition meets computational effects
Proceedings of the 25th Annual Symposium on Logic in Computer Science, Edinburgh, 2010.
LiCS 2010
Revised version (including proofs): Pdf (20 pages)

Monads with arities and their associated theories
with Clemens Berger and Mark Weber.
Journal of Pure and Applied Algebra
Special Issue devoted to the International Conference in Category Theory (CT2010)
Volume 216, Issues 8–9, August 2012, Pages 2029–2048
JPAA 2012
Pdf (31 pages)

Type Theory & Realizability

Constructive Type Theory

A generic proof of strong normalisation for pure type systems
with Benjamin Werner.
Proceedings of the international workshop TYPES'96, Lecture Notes in Computer Science 1512, Springer, 1998.
TYPES'96
PostScript (28 pages)

On the subject reduction property for algebraic type systems
with Gilles Barthe.
Proceedings of the 10th Annual Conference of the European Association for Computer Science Logic, Utrecht
Lecture Notes in Computer Science 1258, pp. 34-57, Springer, 1996.
CSL'96
PostScript (18 pages)

Recursive types and low-level languages

Semantic Types: A fresh look at the ideal models for types
with Jérôme Vouillon,
Proceedings of the 31st Annual Symposium on Principles of Programming Languages, Venezia, 2004.
POPL 2004
PostScript (12 pages)

Recursive polymorphic types and parametricity in an operational framework
with Jérôme Vouillon.
Proceedings of the 21th Conference on Logic in Computer Science, Chicago, 2005.
LiCS 2005
Preliminary version: Pdf (12 pages)

A very modal model of a modern, major, general type system.
with Andrew Appel, Christopher Richards and Jérôme Vouillon.
Proceedings of the 34th Annual ACM Symposium on Principles of Programming Languages, Nice, 2007.
POPL 2007
Preliminary version: Pdf (14 pages)

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders, usually the publishers. All persons and robots copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

The electronic versions of the papers available here may differ from the published versions. The authoritative versions are the published ones.