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
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:
Pdf (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
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)
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
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 Game 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)
Proceedings of the Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science,
Dubrovnik, 2012.
LiCS 2012 Pdf (10 pages)
Dialogue categories and chiralities
Publications of RIMS, Kyoto University 52 (2016), pp. 359-412.
Pdf (57 pages)
The parametric continuation monad
To appear in MSCS, Special Issue dedicated to Corrado Böhm's Anniversary.
Pdf (28 pages)
A micrological study of negation
Annals of Pure and Applied Logic, Volume 168, Issue 2, February 2017.
Pdf (49 pages)
Dialogue categories and Frobenius monoids
Computation, Logic, Games, and Quantum Foundations.
Festschrift in honor of Samson Abramsky for his 60th birthday,
Springer Verlag, LNCS 7860, 2013.
Pdf (49 pages)
On dialogue games and coherent strategies
Proceedings of Computer Science Logic, Torino, 2013.
CSL 2013
Pdf (20 pages)
Une étude micrologique de la négation
Habilitation à Diriger des Recherches
Rapporteurs: Pierre-Louis Curien, André Joyal, Gordon Plotkin
Version préliminaire:
Pdf (294 pages)
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
Pdf (12 pages)
Mathematical Structures in Computer Science, 2016.
Pdf (34 pages).
Monads & Algebraic theories with arities
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)
Local states in string diagrams
Proceedings of the joint conference on Rewriting Techniques and Applications
and Typed Lambda Calculi and Applications.
RTA-TLCA 2014
Pdf (15 pages)
with
Noam Zeilberger.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India, 2015.
POPL 2015
Preliminary version:
Pdf (14 pages)
A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine.
with
Noam Zeilberger.
In Proceedings of the Thirty-First Annual ACM/IEEE Symposium on Logic in Computer Science, New York, 2016.
POPL 2015
Preliminary version:
Pdf (10 pages)
An Isbell duality theorem for type refinement systems.
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
Charles Grellois.
Proceedings of the 18th International Conference on Foundations of Software Science and Computation Structures,
London, 2015.
Fossacs 2015
Pdf (17 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.