Pierre-Louis Curien

Directeur de Recherche au CNRS émérite (depuis octobre 2019)

Membre de l'équipe-projet πr² INRIA commune avec, et du pôle PPS du laboratoire IRIF commun entre le CNRS et l'Université de Paris

Email: curien@irif.fr

Visitez les sites de Nicolas Curien (économiste et chansonnier), Christophe Curien (peintre et sculpteur), et Rémi Curien (géographe et urbaniste), et si votre humeur vous porte vers la culture et l'éveil des plus petits, visitez la BBthèque et la Marmot*thèque de Julie Curien.

Research interests (programming languages, proof theory, algebraic operads and higher categories):

lambda calculi (and explicit substitutions)
typing (in particular: subtyping, parametricity)
domain theory (in particular: sequentiality)
linear logic
game semantics
classical logic
general theory of operads, in particular cyclic operads
higher categories, in particular opetopic ones

A few milestones

PhD thesis in 1979, Doctorat d'État in 1983 (both at Université Paris 7)
1999: Cofounder (with Guy Cousineau, Vincent Danos and Jean-Louis Krivine) of the laboratory "Preuves, Programmes et Systèmes'' (PPS, now part of IRIF)
2009: Cofounder (with Hugo Herbelin) of the Inria joint team πr²
Spring 2014: Coorganiser (with Hugo Herbelin and Paul-André Melliès) of the IHP thematic trimester " Semantics of proofs and certified mathematics"
Editor (since 1989, editor-in-chief since 2016) of the journal Mathematical Structures in Computer science
2020 Grand Prix Inria - Académie des Sciences

Recent prepublications and publications (see also my publication list )

(with Roberto Amadio) Domains and Lambda-calculi, Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (1998) (ABSTRACT).
(with Gérard Boudol and Carolina Lavatelli) A semantics for Lambda-calculi with resources (almost final version), Mathematical Structures in Computer Science 9 (4) (1999).
(with Gordon Plotkin and Glynn Winskel) Bistructure models of linear logic (almost final version) , Milner Festschrift, MIT Press (2000).
Abstract Boehm trees , Mathematical Structures in Computer Science 8(6) (1998).
(with Hugo Herbelin) Computing with abstract Boehm trees (almost final version), Proc. Third Fuji International Symposium on Functional and Logic Programming, April 1998, Kyoto, World Scientific (1998).
Sur l'eta-expansion infinie, Comptes Rendus de l'Académie des Sciences 334, Sec. I, 77-82 (2002).
(with Hugo Herbelin) The duality of computation (almost final version), Proc. International Conference on Functional Programming, September 2000, Montréal, IEEE (2000).
Abstract machines, control, and sequents (almost final version), Proc. APPSEM Summer School, Caminha, Sept. 2000, LNCS 2395, Springer.
Symmetry and interactivity in programming (almost final version), Bulletin of Symbolic Logic, Vol. 9(2), 169-180 (2003).
Sequential algorithms as bistable maps (almost final version), in ''From semantics to computer science: essays in honor of Gilles Kahn'', Cambridge University Press, 51-71 (2009).
Playful, streamlike computation, Proc. Int. Symp. on Domain Theory, Chengdu, 2001, Kluwer.
Introduction to linear logic and ludics, part I, and part II, Advances in Mathematics (China) 34 (5), 513-544 (2005) and 35 (1), 1-44 (2006).
Definability and full abstraction (almost final version), Gordon Plotkin Festschrift, ENTCS 172 (2007).
(with Hugo Herbelin) Abstract machines for dialogue games (final version has appeared in the volume ''Interactive models of computation and program behaviour'', Panoramas et Synthèses 27, Société Mathématique de France (2009).
(with Claudia Faggian) An approach to innocent strategies as graphs (almost final version), Information and Computation 214, 119-155 (2012).
(with Vincent Danos, Jean Krivine, and Zhang Min) Computational self-assembly (almost final version), Theoretical Computer Science 404 (1-2), 61-75 (2008).
Operads, clones, and distributive laws (almost final version), Proc. of the International Conference on Operads and Universal Algebra, Nankai Series in Pure, Applied Mathematics and Theoretical Physics, Vol. 9, World Scientific, Singapore, 25-50 (2012).
(with Guillaume Munch-Maccagnoni) The duality of computation under focus, version of June 2010, slightly more expanded than the version published in the Proc. of IFIP TCS Conference 2010, IFIP Advances in Information and Communication Technology, vol. 323, Springer (2010).
(with Richard Garner and Martin Hofmann) Revisiting the categorical interpretation of type theory (almost final version), Theoretical computer Science 546, 99-119 (special issue in honor of G. Winskel's 60th birthday) (2014).
(with M. Fiore and G. Munch) A theory of effects and resources: adjunction models and polarised calculi (almost final version), Principles of Programming Languages 2016.
(with E. Burgunder and M. Ronco) Free algebra structures on the permutohedra (almost final version), Journal of Algebra 487, 20-59 (2017).
(with S. Mimram) Coherent presentations of monoidal categories, Logical Methods in Computer Science 13 (3) (2017).
(with J. Obradović) A formal language for cyclic operads, Higher Structures 1(1), 22-55 (2017).
(with J. Obradović and J. Ivanović) Syntactic aspects of hypergraph polytopes (almost final version), Journal of Homotopy and Related Structures 14(1), 235-279 (2019).
(with J. Obradović) Categorified cyclic operads. Applied Categorical Structures 28, 59–112 (2020).
(with D. Baralić, M. Milicević, J. Obradović, Z. Petrić, M. Zekić, R. Zivaljević) Proofs and surfaces, Annals of Pure and Applied Logic 171 (9), 42p. (2020).
(with C. Ho Thanh and S. Mimram) Syntactic approaches to opetopes.

Some older publications

Sequential algorithms on concrete data structures, Theoretical Computer Science 20, 265-321 (1982).
Substitution up to isomorphism, Fundamenta Informaticae 19, 51-85 (1993).
(with Martin Abadi, Luca Cardelli and Jean-Jacques Lévy) Explicit substitutions, Journal of Functional Programming 1(4), 375-416 (1992).
(with Martin Abadi and Luca Cardelli)) Formal parametric polymorphism, Boehm Festschrift Volume, Theoretical Computer Science 121 (1-2), 9-58 (1993).

Introductory course notes

Introductory slides to ludics for the Spring School in Agay, March 2002.

Introduction to CCS and pi-calculus (still incomplete notes), December 2002.
Notes on game semantics, September 2006.
Category theory: a programming language introduction, version of 20/10/08.
CIRM 2014 lectures on categories for programming languages, April 2014.
ECI 2021 course "Introduction to homotopy type theory" (slides available here).

Biographie scientifique et hommages

Une brève biographie scientifique de Maurice Nivat, special issue of TCS dedicated to Maurice Nivat, Theoretical Computer Science 281 (1-2) (2002).
Patrick Dehornoy au prisme de l’informatique fondamentale, Gazette des Mathématiciens, Tome 164 (2020).

Vulgarisation

Une brève biographie scientifique de Maurice Nivat, special issue of TCS dedicated to Maurice Nivat, Theoretical Computer Science 281 (1-2) (2002).
Patrick Dehornoy au prisme de l’informatique fondamentale, Gazette des Mathématiciens, Tome 164 (2020).

Teaching

Cours de théorie de la démonstration, première partie et compléments, M2 LMFI.
Poly (partiel, inachevé) de Cours de Magistère.
Documents de travail 1999 , et 2000 pour l'Oral d'Informatique aux concours d'entrée aux ENS (Cachan, Lyon, Ulm en 1999; Lyon, Ulm en 2000).
Documents for the course "Homotopical algebra and higher categories" (master 2 LMFI course 2020/2021, Université de Paris) available here.

Some talks

Sémantique opérationnelle (avril 2001, transparents et texte).
Games in computer science: a survey (talk at Moscow Independent University, April 2005).
An approach to innocent strategies as games (slides for an invited contribution at the workshop Current trends in Concurrency Theory, Ecole Polytechnique, Nov. 2006).
What can sequent calculus do for functional programs? (talk at the Computer Lab., Cambridge, June 2009).
System L syntax for sequent calculi (talk at the University of Bath, at PPS, at Ecole Polytechnique, version of May 4, 2012).
La traque des bugs en informatique (Café des Sciences, Alliance Française et Consulat de France, Wuhan, 29/4/2015).
Sequential interactive behaviour of recursive program schemes (talk at Journées Calculabilité 2016 of the GDR IM, Nice, in April 2016, and at Tallinn University of Technology in December 2017).
Sequential algorithms and innocent strategies share the same execution mechanism (talk at the workshop Games for Logic and Programming Languages (GaLoP) 2019, Prague, April 2019).