Pierre Clairambault

CNRS researcher (CR), member of the Plume team in the LIP laboratory, at ENS Lyon.

Member of the CoNRS, Section 6.

Email : pierre.clairambault@ens-lyon.fr
Équipe Plume Laboratoire de l'Informatique du Parallélisme ENS de Lyon 46 allée d'Italie 69364 Lyon

Research Interests

Semantics of logics and programming languages. Denotational semantics, game semantics.
Concurrency.
Applications of semantics in programming languages and their verification.
Categorical and logical methods in computer science.
Dependent type theory.

News

Check out the Concurrent Games Café!
New ANR project DyVerSe.

Preprints

Pierre Clairambault. A Tale of Additives and Concurrency in Game Semantics. [pdf]
Simon Castellan, Pierre Clairambault and Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed. [pdf, arXiv]
Pierre Clairambault. Learning to Count up to Symmetry. [pdf, HAL]
Simon Castellan and Pierre Clairambault, Disentangling Parallelism and Interference in Game Semantics. [pdf]

Publications in conferences

Pierre Clairambault and Marc de Visme. Full Abstraction for the Quantum Lambda-Calculus.
In POPL 2020. [pdf]
Pierre Clairambault and Andrzej Murawski. On the expressivity of linear recursion schemes.
In MFCS 2019. [HAL]
Aurore Alcolei, Pierre Clairambault and Olivier Laurent. Resource-Tracking Concurrent Games.
In FoSSaCS'19. [HAL]
Pierre Clairambault, Marc de Visme, and Glynn Winskel. Game Semantics for Quantum Programming.
In POPL 2019. [pdf]
Aurore Alcolei, Pierre Clairambault, Martin Hyland, and Glynn Winskel. The True Concurrency of Herbrand's Theorem.
In CSL 2018. [pdf, HAL]
Pierre Clairambault and Hugo Paquet. Fully abstract models of the probabilistic lambda-calculus.
In CSL 2018. [HAL]
Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The concurrent game semantics of Probabilistic PCF.
In LICS 2018. [pdf, HAL]
Simon Castellan, Pierre Clairambault, Jonathan Hayman and Glynn Winskel. Non-angelic concurrent game semantics.
In FOSSACS'18. [pdf, HAL]
Pierre Clairambault, Charles Grellois and Andrzej Murawski. Linearity in Higher-Order Recursion Schemes.
In POPL 2018. [pdf, HAL, talk]
Simon Castellan, Pierre Clairambault, and Glynn Winskel. Distributed Strategies Made Easy.
In MFCS 2017 (Invited paper). [HAL]
Simon Castellan, Pierre Clairambault, and Glynn Winskel. Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or.
In FSCD 2017. [pdf, HAL]
Simon Castellan and Pierre Clairambault. Causality vs. interleavings in concurrent game semantics.
In CONCUR 2016. [pdf, HAL]
Simon Castellan, Pierre Clairambault and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category.
In TLCA 2015. [pdf, HAL]
Simon Castellan, Pierre Clairambault and Glynn Winskel. The parallel intensionally fully abstract model of PCF.
In LICS 2015. [pdf, HAL]
Pierre Clairambault and Peter Dybjer. Game semantics and normalization by evaluation.
In FOSSACS 2015, [pdf, HAL]
Simon Castellan, Pierre Clairambault and Glynn Winskel. Symmetry in concurrent games.
In CSL-LICS 2014. [pdf, HAL]
Pierre Clairambault and Andrzej Murawski. Böhm trees as Higher-Order Recursion Schemes.
In FSTTCS 2013. [pdf, HAL]
Pierre Clairambault and Glynn Winskel. On concurrent games with payoff.
In MFPS 2013. [pdf]
Pierre Clairambault. Locally Scoped Terms, Bounding Skeletons and Exact Bounds for Head Reduction.
In TLCA 2013. [pdf]
Pierre Clairambault, Julian Gutierrez, and Glynn Winskel. The winning ways of concurrent games.
In LICS 2012. [pdf]
Pierre Clairambault and Peter Dybjer. The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories.
In TLCA 2011. [pdf, HAL, arXiv]
Pierre Clairambault. Isomorphisms of types in the presence of higher-order references
In LICS 2011. [pdf, HAL, arXiv]. Look here for an isomorphism of types in OCaml between int -> int -> unit and int -> unit
Pierre Clairambault. Estimation of the length of interactions in arena game semantics
In FOSSACS 2011. [pdf, HAL, arXiv]
Pierre Clairambault. Least and Greatest Fixpoints in Game Semantics.
In FOSSACS 2009. [pdf, HAL, arXiv]

Publications in journals

Simon Castellan, Pierre Clairambault and Glynn Winskel. Thin Games with Symmetry and Concurrent Hyland-Ong Games. In Logical Methods in Computer Science. [pdf]
Simon Castellan, Pierre Clairambault and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category (extended version).
In Logical Methods in Computer Science, 2017. [pdf, HAL]
Simon Castellan, Pierre Clairambault, Silvain Rideau and Glynn Winskel. Games and Strategies as Event Structures.
In Logical Methods in Computer Science, 2017. [pdf, HAL, arXiv]
Pierre Clairambault. Bounding linear head reduction and visible interaction through skeletons.
In Logical Methods in Computer Science, 2015. [pdf, HAL, arXiv]
Pierre Clairambault and Peter Dybjer. The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories.
In Mathematical Structures in Computer Science, 2014. [pdf, HAL, erratum]
Pierre Clairambault, Julian Gutierrez and Glynn Winskel. Imperfect information in logic and concurrent games.
In Computation, Logic, Games, and Quantum Foundations - The Many Facets of Samson Abramsky: Essays Dedicted to Samson Abramsky on the Occasion of His 60th Birthday (Lecture Notes in Computer Science) , 2013.
Pierre Clairambault. Strong functors and interleaving fixpoints in game semantics
In Theoretical Informatics and Applications, 2013. [pdf]
Pierre Clairambault. Isomorphisms of types in the presence of higher-order references (extended version).
In Logical Methods in Computer Science (selected papers of LICS 2011), 2012. [pdf].
Pierre Clairambault and Russ Harmer. Totality in Arena Games
In Annals of Pure and Applied Logic, 2010. [pdf, HAL]

PhD thesis

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

Software

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