Pierre Clairambault's page

Researcher at the CNRS, member of the Plume team in the LIP laboratory, in the ENS de Lyon.

I did my PhD thesis in the PPS laboratory in Paris, under the supervision of Russ Harmer and Pierre-Louis Curien. After that, I did a postdoc in the Department of Computer Science of the University of Bath with Jim Laird, then a postdoc in the Computer Laboratory of the University of Cambridge, with Glynn Winskel.

Member of the CoNRS, Section 6.

News

• In 2017, I am teaching a M2 course at ENS Lyon on Models of concurrency, categories, and games, jointly with Glynn Winskel.

In preparation / submitted

• The True Concurrency of Herbrand's Theorem, with Aurore Alcolei, Martin Hyland, and Glynn Winskel. Submitted. [pdf]
• Forgetting causality in the concurrent game semantics of probabilistic PCF, with Simon Castellan, Hugo Paquet, and Glynn Winskel. Submitted. [pdf]
• Non-angelic concurrent game semantics, with Simon Castellan, Jonathan Hayman, and Glynn Winskel. Submitted. [pdf]
• Concurrent Hyland-Ong Games, with Simon Castellan and Glynn Winskel. Submitted. [pdf, arxiv]

Accepted

• Linearity in Higher-Order Recursion Schemes, with Charles Grellois and Andrzej Murawski. Accepted to POPL 2018.
• Undecidability of Equality in the Free Locally Cartesian Closed Category (extended version), with Simon Castellan and Peter Dybjer. Accepted to the special issue of TLCA 2015, LMCS; 2017. [pdf]

Publications

• Games and Strategies as Event Structures, with Simon Castellan, Silvain Rideau, and Glynn Winskel. LMCS, 2017. [pdf, arxiv]
• Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or, with Simon Castellan and Glynn Winskel, FSCD 2017. [pdf]
• Causality vs. interleavings in concurrent game semantics, with Simon Castellan. CONCUR 2016. [pdf]
• Undecidability of Equality in the Free Locally Cartesian Closed Category, with Simon Castellan and Peter Dybjer, TLCA 2015. [pdf]
• The parallel intensionally fully abstract model of PCF, with Simon Castellan and Glynn Winskel, LICS 2015. [pdf]
• Bounding linear head reduction and visible interaction through skeletons, LMCS, 2015. [pdf]
• Game semantics and normalization by evaluation, with Peter Dybjer, FOSSACS 2015, [pdf]
• Symmetry in concurrent games, with Simon Castellan and Glynn Winskel, CSL-LICS'14. [pdf]
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, with Peter Dybjer, MSCS, 2014. [pdf, erratum]
• On concurrent games with payoff, with Glynn Winskel, MFPS 2013. [pdf].
• Böhm trees as Higher-Order Recursion Schemes, with Andrzej Murawski, FSTTCS 2013. [pdf]
• Locally Scoped Terms, Bounding Skeletons and Exact Bounds for Head Reduction, TLCA 2013 [pdf].
• Imperfect information in logic and concurrent games, with Julian Gutierrez and Glynn Winskel, in the Festschrift for the 60th birthday of Samson Abramsky.
• Strong functors and interleaving fixpoints in game semantics, Theoretical Informatics and Applications, 2013 [pdf].
• Isomorphisms of types in the presence of higher-order references (extended version), selected papers of LICS 2011, Logical Methods in Computer Science, 2012. [pdf].
• The winning ways of concurrent games, with Julian Gutierrez and Glynn Winskel, LICS 2012. [pdf].
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, with Peter Dybjer, TLCA'11. [pdf, hal, arxiv].
• Isomorphisms of types in the presence of higher-order references, LICS'11. [pdf, hal, arxiv]. Look here for an isomorphism of types in OCaml between int -> int -> unit and int -> unit
• Estimation of the length of interactions in arena game semantics, FOSSACS'11. [pdf, hal, arxiv].
• Least and Greatest Fixpoints in Game Semantics 2 : strong functors and interleaving types, in the proceedings of FICS09. [pdf]
• Totality in Arena Games, with Russ Harmer. Annals of Pure and Applied Logic. [pdf, hal]
• Least and Greatest Fixpoints in Game Semantics. FOSSACS'09. [pdf, hal, arxiv]

PhD thesis

• Logique et Interaction : une Étude Sémantique de la Totalité. [pdf, tel,slides], defended on the 19th of February, 2010.

Unpublished notes and reports

• Concurrent Hyland-Ong games. [arXiv]
• Laird's triggering/blocking games model is equivalent to Conway games. [pdf]
• About normalization in HO games semantics, using the Pointer Abstract Machine [pdf]
• My DEA report on game semantics and decidability of equivalence for fragments of PCF (in french) [pdf]
• My M1 report on categorical models of type theory. [pdf].
• My L3 report about proofs of probabilistic programs in COQ (in french). [pdf]

Programming

• See here a simulator for Hyland-Ong game semantics, generating interaction traces between terms of PCF.