Research

This list includes research articles as well as unpublished notes
on my various research interests.
If you are in that mood, you are also welcome to visit the page dedicated to tensorial logic
and template games.

2015 - 2020

**Concurrent separation logic meets template games.** [pdf]

With Léo Stefanesco. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'20.

**On bifibrations of model categories.**
[pdf]
[bib]

With Pierre Cagne. Advances in Mathematics, Volume 370, 26 August 2020.

**Comprehension and quotient structures in the language of 2-categories.** [pdf]

With Nicolas Rolland. Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020.

**A functorial excursion between algebraic geometry and linear logic.** [pdf]

Submitted manuscript, 2020.

**Template games and differential linear logic.** [pdf]
[bib]
[page]

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'19.

**Categorical combinatorics of scheduling and synchronization in game semantics.** [pdf]
[bib]
[slides]
[video]
[page]

Proceedings of the 46th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL'19.

**Ribbon tensorial logic.** [pdf]
[bib]
[page]

Proceedings of the 33th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18.

**Categorical combinatorics for non deterministic strategies on simples games.**
[pdf]
[bib]

With Clément Jacq. Proceedings of 21st International Conference on the Foundations of Software Science and Computation Structures, FoSSaCS'18.

**An asynchronous soundness theorem for concurrent separation logic.** [pdf]
[bib]

With Leo Stefanesco. Proceedings of the 33th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18.

**An explicit formula for the free exponential modality of linear logic.**
[pdf] [bib]

With Nicolas Tabareau and Christine Tasson.
Mathematical Structures in Computer Science 28(7): 1253-1286 (2018)

**An Isbell duality theorem for type refinement systems.** [pdf] [bib]

With Noam Zeilberger. Mathematical Structures in Computer Science 28(6): 736-774 (2018)

**Higher-order parity automata.** [pdf]
[bib]
[slides]

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'17.

**A micrological study of negation.** [pdf]
[bib]
[page]

Annals of Pure and Applied Logic 168(2): 321-372 (2017)

**The parametric continuation monad.** [pdf]
[bib]

Mathematical Structures in Computer Science 27(5): 651-680 (2017)

**A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine.**
[pdf]
[bib]

With Noam Zeilberger.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16.

**Five basic concepts of Axiomatic Rewriting Theory.**
[pdf]
[slides]

Invited talk at the 5th International Workshop on Confluence, IWC'16.

**Towards a formal theory of graded monads.**
[pdf]
[bib]

With Soichiro Fujii and Shin-ya Katsumata. 19th International Conference on the Foundations of Software Science and Computation Structures, FoSSaCS'16.

**Dialogue categories and chiralities.**
[pdf]
[bib]

Publications of the Research Institute in Mathematical Science (RIMS), 2016.

2010 - 2015

**A fibrational account of local states.**
[pdf]
[bib]

With Kenji Maillard.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'15.

**Functors are type refinement systems.**
[pdf]
[bib]

With Noam Zeilberger.
Proceedings of the 42nd ACM SIGPLAN Symposium on Principles of Programming Languages, POPL'15.

**Finitary semantics of linear logic and higher-order model checking.**
[pdf]
[bib]

With Charles Grellois.
40th International Symposium on the Mathematical Foundations of Computer Science, MFCS'15.

**Relational semantics of linear logic and higher-order model checking.**
[pdf]
[bib]

With Charles Grellois.
24th EACSL Annual Conference on Computer Science Logic, CSL'15.

**An infinitary model of linear logic.**
[pdf]
[bib]

With Charles Grellois.
18th International Conference on the Foundations of Software Science and Computation Structures, FoSSaCS'15.

**Local states in string diagrams.**
[pdf]
[bib]

Proceedings of Rewriting and Typed Lambda Calculi, Joint International Conference, RTA-TLCA 2014.

**Indexed linear logic and higher-order model checking.**
[pdf]
[bib]

With Charles Grellois. Seventh International Workshop on Intersection Types and Related Systems, ITRS 2014.

**On dialogue games and coherent strategies.**
[pdf]
[bib]

Proceedings of the 22nd Annual EATCS Conference on Computer Science Logic, CSL 2013.

**Type refinement and monoidal closed bifibrations.**
[pdf]
[bib]

With Noam Zeilberger. Unpublished manuscript, 2013.

**Monads with arities and their associated theories.**
[pdf]
[bib]

With Clemens Berger and Mark Weber. Journal of Pure and Applied Algebra, 2012.

**Game semantics in string diagrams.**
[pdf]
[bib]

Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'12.

**Resource modalities in tensor logic.**
[pdf]
[bib]

Annals of Pure and Applied Logic 161(5): 632-653, 2010.

**Segal condition meets computational effects.**
[pdf]
[bib]

Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS'10.

2005 - 2010

**An explicit formula for the free exponential modality of linear logic.**
[pdf]
[bib]

With Nicolas Tabareau and Christine Tasson. Proceedings of the 36th international Colloquium on Automata, Languages and Programming, ICALP 2009.

**An algebraic account of references in game semantics.**
[pdf]
[bib]

With Nicolas Tabareau. Proceedings of the 25th Conference on Mathematical Foundations of Programming Semantics, MFPS 2009.

**Asynchronous games: innocence without alternation.**
[pdf]
[bib]

With Samuel Mimram. Proceedings of the 18th International Conference on Concurrency Theory, CONCUR 2007.

**Resource modalities in game semantics.**
[pdf]
[bib]

With Nicolas Tabareau. Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, LICS'07.

**Categorical combinatorics for innocent strategies.**
[pdf]
[bib]

With Russ Harmer and Martin Hyland. Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, LICS'07.

**A very modal model of a modern, major, general type system.**
[pdf]
[bib]

With Andrew Appel, Christopher D. Richards and Jérôme Vouillon. Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007.

**Asynchronous games 2: the true concurrency of innocence.**
[pdf]
[bib]

Theoretical Computer Science 358(2-3): 200-228, 2006.

**Functorial boxes in string diagrams.**
[pdf]
[bib]

Invited paper at the 20th International Workshop on Computer Science Logic, CSL'06.

**Sequential algorithms and strongly stable functions.**
[pdf]
[bib]

Theoretical Computer Science 343(1-2): 237-281, 2005.

**Asynchronous games 3: an innocent model of linear logic.**
[pdf]
[bib]

Proceedings of the 10th International Conference on Categorical Structures in Computer Science, CTCS'05.

**Axiomatic Rewriting Theory I: A Diagrammatic Standardization Theorem.**
[pdf]
[bib]

Processes, Terms and Cycles: Essays Dedicated to Jan Willem Klop, 554-638, 2005.

**Recursive Polymorphic Types and Parametricity in an Operational Framework.**
[pdf]
[bib]

With Jérôme Vouillon. Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS'05.

**Asynchronous Games 4: A Fully Complete Model of Propositional Linear Logic.**
[pdf]
[bib]

Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS'05.

before 2005

**Comparing hierarchies of types in models of linear logic.**
[pdf]
[bib]

Information and Computation, 189(2): 202-234, 2004.

**Asynchronous Games 2: The True Concurrency of Innocence.**
[pdf]
[bib]

Proceedings of the 15th International Conference on Concurrency Theory, CONCUR 2004.

**Semantic types: a fresh look at the ideal model for types.**
[pdf]
[bib]

With Jérôme Vouillon. Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004.

**Double Categories: A Modular Model of Multiplicative Linear Logic.**
[pdf]
[bib]

Mathematical Structures in Computer Science 12(4): 449-479, 2002.

**Axiomatic Rewriting Theory VI: Residual Theory Revisited.**
[ps]
[pdf]
[bib]

13th International Conference on Rewriting Techniques and Applications, RTA'02.

**Axiomatic Rewriting Theory II: the lambda-sigma-calculus enjoys finite normalisation cones.**
[pdf]
[bib]

Journal of Logic and Computation, 10(3): 461-487, 2000.

**Concurrent Games and Full Completeness.**
[pdf]
[bib]

With Samson Abramsky. Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS'99.

**On a Duality Between Kruskal and Dershowitz Theorems.**
[pdf]
[bib]

Proceedings of the 25th International Colloquium on Automata, Languages and Programming, ICALP'98.

**Axiomatic Rewriting Theory IV : A Stability Theorem in Rewriting Theory.**
[ps]
[pdf]
[bib]

Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, LICS'98.

**Axiomatic Rewriting Theory III : A Factorisation Theorem in Rewriting Theory. **
[ps]
[pdf]
[bib]

Proceedings of the 7th International Conference on Category Theory and Computer Science, CTCS'97.

**On the Subject Reduction Property for Algebraic Type Systems. **
[ps]
[pdf]
[bib]

With Gilles Barthe. Proceedings of the 10th International Workshop on Computer Science Logic, CSL'96.

**A Generic Normalisation Proof for Pure Type Systems. **
[ps]
[pdf]
[bib]

With Benjamin Werner. International Workshop on Types for Proofs and Programs, TYPES'96.

**Typed lambda-calculi with explicit substitutions may not terminate. **
[ps]
[pdf]
[bib]

Second International Conference on Typed Lambda Calculi and Applications, TLCA'95.

**An abstract standardisation theorem.**
[ps]
[pdf]
[bib]

With Georges Gonthier and Jean-Jacques Lévy.
Proceedings of the Seventh Annual Symposium on Logic in Computer Science, LICS'92.

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.