Convolution products on double categories and categorification of rule algebra.
with Nicolas Behr and Noam Zeilberger. Proceedings of the 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023.

Profinite lambda-calculus and parametricity. [pdf]
with Sam van Gool and Vincent Moreau. Proceedings of the 39th Conference on Mathematical Foundations of Programming Semantics, MFPS 2023.

Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem. [pdf]
with Noam Zeilberger. To appear in the Proceedings of the 38th International Conference on Mathematical Foundations of Programming Semantics, MFPS 2022.

A functorial excursion between algebraic geometry and linear logic. [pdf]
Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'22.

Layered and Object-Based Game Semantics. [pdf] [bib]
with Arthur Oliveira Vale, Zhong Shao, Jérémie Koenig, and Léo Stefanesco. Proceedings of the 49th ACM Symposium on Principles of Programming Languages (PACMPL), Volume 6, PoPL'22.

Asynchronous template games and the Gray tensor product of 2-categories. [pdf] [bib] [slides] [video]
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'21.

Concurrent separation logic meets template games. [pdf] [bib]
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] [bib]
With Nicolas Rolland. Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, FSCD 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 Game Semantics of Concurrent Separation Logic. [pdf] [bib]
With Leo Stefanesco. Proceedings of Mathematical Foundations of Programming Semantics, MFPS 2017, Electronic Notes in Theoretical Computer Science 336, Elsevier 2018.

On Dialogue Games and Graph Games. [pdf] [bib]
With Clément Jacq. Proceedings of Mathematical Foundations of Programming Semantics, MFPS 2017, Electronic Notes in Theoretical Computer Science 336, Elsevier 2018.

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.

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.

Dialogue categories and Frobenius monoids. [pdf] [bib] [slides] [video]
Computation, Logic, Games, and Quantum Foundations -- Essays Dedicated to Samson Abramsky on the Occasion of His 60th Birthday,
Lecture Notes in Computer Science, volume 7860, Springer, 2013.

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.

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.

Comparing hierarchies of types in models of linear logic. [pdf] [bib]
Information and Computation, 189(2): 202-234, 2004.

A topological correctness criterion for non-commutative linear logic. [pdf] [bib]
Thomas Ehrhard, Jean-Yves Girard, Paul Ruet and Philip Scott editors. Linear Logic in Computer Science, CambridgeUniversity Press, pp.283-323, 2004, London Mathematical Society, Lecture Note Series 316.

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.