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.

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.

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

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 regulating programs and strategies is described using 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 more on that topic on this web page.

I have spent most of my summer time 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 nice atmosphere in Bonn during the trimester, with a lot of inspiring talks and lively discussions between us.

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 last November. 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.

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.