IRIF
Fondation des Sciences Math´matiques
Federation Paris 7
CNRS


Paul-André Melliès

Welcome to my home page. I am a CNRS Researcher member of the Laboratoire IRIF at the Department of Mathematical Sciences and Department of Computer Science of the Université Paris Denis Diderot.

Research Interests

Mathematical logic, proof theory, game semantics, theory and practice of programming languages, computer architecture, operating systems, formalized mathematics, proof assistants, mathematical physics, knot theory, quantum groups, n-dimensional algebra, operads. My ambition is to connect these topics.

Where to find me

Institut de Recherche en Informatique Fondamentale (IRIF)
Office 3023
Bâtiment Sophie Germain
Université Paris Diderot, case 7014
5, rue Thomas Mann
75205 Paris Cedex 13
FRANCE

phone: 00 33 1 57 27 92 48
fax: 00 33 1 57 27 92 97

email: mellies@irif.fr

Recent papers and drafts (more on dblp and here)

Asynchronous template games and the Gray tensor product of 2-categories. [pdf]
Submitted manuscript, 2021.

A functorial excursion between algebraic geometry and linear logic. [pdf]
Submitted manuscript, 2021.

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.

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.

On bifibrations of model categories. [pdf] [bib]
With Pierre Cagne. Advances in Mathematics, Volume 370, 26 August 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.

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.

Books and surveys

Une étude micrologique de la négation. [pdf] [slides] [bib] [page]
Habilitation à diriger des recherches, 2017 (291 pages, in French).

Categorical semantics of linear logic. [pdf] [bib] [page]
Panoramas et Synthèses, Société Mathématique de France, 2009 (213 pages).

A few videos, old and new

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.

A knotty introduction to tensorial logic and dialogue categories. [slides] [video]
Invited talk at the workshop Proofs and Computations held during the Types, Sets and Constructions Trimester Programme organized at the Hausdorff Research Institute for Mathematics, July 2018.

Refinement type systems and Martin-Löf type theory. [slides] [video]
Invited talk at the workshop Types, Homotopy Type theory, and Verification held during the Types, Sets and Constructions Trimester Programme organized at the Hausdorff Research Institute for Mathematics, June 2018.

Dialogue categories and Frobenius monoids. [pdf] [slides] [video]
Invited paper and talk at Samson@60 in honour of Samson Abramsky, 2013.

Programming languages in string diagrams. [A] [1] [2] [B] [3] [C] [4] [5] [6]
Invited talk at the 10th annual Oregon Programming Languages Summer School, June 2011.

Announcements

I was delighted to give a talk at this extremely nice and inspiring Combinatory and Arithmetics for Physics 2020 conference organized (virtually!) at IHES on the 2nd and 3rd of December by Gérard H. E. Duchamp, Maxim Kontsevich, Gleb Koshevoy and Hoang Ngoc Minh. I was speaking more specifically about the connection between ribbon tensorial logic, Hopf algebras and balanced dialogue categories. You are welcome to look at my slides here. The conference was a lot of fun and full of very interesting talks. You will find more about them in this timetable.

I am taking part and organize the new and exciting workshop GeoCat 2020 on the geometric and categorical structures in computation and deduction. The workshop will take place online on Saturday 4 July and Sunday 5 July as satellite to the FSCD 2020 conference. Do not hesitate to contact me if you want to know more about the event.



I was delighted to take part to the workshop Logic and Structure in Computer Science and Beyond (LSCSB) organized at the Lorentz Center in Leiden this December. The working atmosphere was excellent and I was impressed by a number of recent groundbreaking advances in our field.

I was delighted to take part to Circularity in Syntax and Semantics organized in Göteborg this November, and to give on that occasion an invited talk about my recent work on higher-order parity automata. You will find the slides of my talk here.

One important issue in programming language semantics and concurrency theory is to understand how two programs synchronize and interact together, in a safe and modular way. I am currently working on a notion of template game where the scheduling policy which regulates programs and strategies is described by an independent algebraic structure, called a synchronization template. One benefit of the approach is that template games come in different flavour (sequential, concurrent, relational) depending on the chosen synchronization template. You will find on this web page a number of papers and talks dedicated to template games, and in particular the description of a homotopy model of differential linear logic.

I am currently finishing a paper with Nicolas Rolland exploring the categorical semantics of inductive and coinductive reasoning (formulated in initial algebras and final coalgebras) in type refinement systems. The paper is on the way of completion and you will find it here very soon!

I have spent most of my summer 2018 in Bonn (Germany) at the Hausdorff Research Institute for Mathematics where I took part to the thematic trimester on Types, Sets and Constructions organized by Douglas S. Bridges, Michael Rathjen, Peter Schuster and Helmut Schwichtenberg. Have a look at the program of the first workshop of the HIM trimester if you are interested in types, and more specifically in homotopy types and their application to proof assistants and higher categories. A wonderful atmosphere in Bonn during the trimester, with a lot of inspiring talks and lively discussions between us.


Types, Sets and Constructions

End of August, I took part to that summer school organized by Florent Krzakala and Lenka Zdeborova in Cargese on the connection between statistical physics and machine learning. A wonderful occasion for me to learn more about these two topics and how to combine them harmoniously. Knowledge is fun!

I have just taken part to the Paris Symposium on Games 2018 and given an invited talk on a number of new and exciting ideas which came to me quite recently, building on my ancient work on asynchronous games. More about all this soon...

I believe that the connection between logical proofs and topological knots can teach us a lot -- both at the abstract mathematical level and at the very concrete level of memory management. If you are curious to know more about this emerging and entertaining topic, please have a look here at my recent paper on ribbon tensorial logic. The paper has been presented this July at the LICS 2018 conference.

I am very interested in understanding how concurrent separation logic works to ensure that imperative and concurrent programs with locks are correct -- and in particular that they do not produce data races. I have been working hard with Léo Stefanesco to define an asynchronous game semantics for the logic. Please have a look at our recent paper here and tell us what you think! The paper has been presented this July at the LICS 2018 conference.

I have defended my habilitation thesis in November 2017. You will find a version of the manuscript (in French) here.

You will also find on this web page a series of recent papers on tensorial logic. Your comments are most welcome!

If you are interested in higher-order model-checking, please have a look at my recent LICS 2017 paper where ideas coming from linear logic and infinitary rewriting are combined to define a notion of higher-order parity automaton.

I have given an invited talk on axiomatic rewriting at IWC 2016. If you are interested to know more about the five basic concepts of the theory, please have a look at the abstract and at the slides here and here.


Abelard and Eloise

Past events

I have taken part to this workshop on higher topological quantum field theory and categorical quantum mechanics at the Schrödinger Institute in Vienna. I spoke about the correspondance between dialogue categories and a 2-categorical (and lax) version of Frobenius algebra. You will find the slides of my talk here.

If you are interested to see how memory can be depicted in string diagrams, you will find here a preliminary version of my RTA-TLCA 2015 paper.

Please have a look here at the preliminary version of my paper with Noam Zeilberger which was presented at the POPL 2015 conference. You may be also interested to read this more recent paper on a Isbell duality theorem for type refinement systems.

The book with Pierre-Louis Curien and Jean-Louis Krivine at the interface between mathematical logic and programming languages semantics is finished. My own section, devoted to the categorical semantics of linear logic, appears here.

I have organized with Pierre-Louis Curien and Hugo Herbelin the thematic trimester Semantics of proofs and certified mathematics which has been hosted at the Institut Henri Poincaré during this spring 2014, from April 22 to July 11.

I was in Marseille for the thematic week on Proofs and programs organized at CIRM as part of Logic and interactions 2012. I then took take part to the last thematic week, devoted this time to Algebra and computation.

I gave a series of four lectures at the Oregon Programming Languages Summer School. You may have a look at the slides and videos of the lectures here.

You may have a look at my LICS paper on computational effects and the Segal condition, including an algebraic reconstruction of the state monad after Plotkin and Power.

Nick Benton and I organize the workshop LOLA devoted to the syntax and the semantics of low level languages. This satellite workshop of the LICS conference will take place at Edinburgh on July 9, 2010.

Andrzej Murawski, Andrea Schalk, Igor Walukiewicz and I organize a summer school on Game Semantics and Program Verification which will take place at Dagstuhl from June 20 to June 25, 2010.

I gave a series of three lectures at the Hopf-in-Lux conference on Hopf algebras, which took place in Luxembourg, from July 13 to July 17, 2009.

I was an invited speaker of the Topology, Algebra and Categories in Logic conference, which took place in Amsterdam, from July 7 to July 11, 2009.

The 60th birthdays of Martin Hyland and Peter Johnstone have been celebrated during the recent Peripatetic Seminar on Sheaves and Logic taking place in Cambridge on April 4 and 5, 2009.

I was invited by the Logic and Geometry of Cognition group in Roma Tre, to give a week-long course on 2-dimensional algebra and string diagrams for PhD students and researchers coming from logical and mathematical backgrounds. The slides appear here.

I was an invited speaker at the workshop on Games for Logic and Programming Languages (GaLoP) which will take place from 29 March to 6 April 2008 in Budapest.

In April 2007, I was an invited speaker at the Fields Institute workshop Recent advances in category theory and logic: Applications of traces to algebra, analysis and categorical logic in Ottawa.

In May 2007, I was an invited speaker at the workshop Linear Logic, Ludics, Implicit Complexity, Operator Algebras in Siena, celebrating the 60th birthday of the French logician Jean-Yves Girard.

I was a member of the Programme Committee of the Computer Science and Logic conference which took place in Lausanne, in September 2007.

I took part to the Summer School on Contemporary Categorical Methods in Algebra and Topology which took place in June 2007 in Hautes-Bodeux, a small village in the middle of the belgian Ardennes.

Together with Anca Muscholl, I organized the Ecole de Printemps en Informatique Théorique devoted to Games in Semantics and Verification. The event took place at l'Ile de Ré in June 2006.

 

Vivre et créer à Paris

Surpris par la nuit