Pierre Clairambault's page

I did my PhD thesis in the PPS laboratory. My advisors were Russ Harmer and Pierre-Louis Curien. I spent one year as a postdoctoral researcher in the Department of Computer Science of the University of Bath. I am now working in the Computer Laboratory of the University of Cambridge, within the ERC Advanced Grant ECSYM.

News

• I was invited speaker in the 7th edition of the workhop GaLoP in Dubrovnik on June 29, 2012, affiliated with LICS 2012.
• I was member of the PC of the 6th edition of the workshop GaLoP in Saarbrucken on March 26-27 2011, affiliated with ETAPS 2011.

In preparation

• On concurrent games with symmetry, with Simon Castellan and Glynn Winskel, Submitted.
• Böhm trees as Higher-Order Recursion Schemes, with Andrzej Murawski, Submitted.
• The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, with Peter Dybjer, in revision for MSCS. [pdf (preliminary version)].

Publications

• On concurrent games with payoff, with Glynn Winskel, to appear in the proceedings of MFPS'13. [pdf (preliminary version)].
• Locally Scoped Terms, Bounding Skeletons and Exact Bounds for Head Reduction, to appear in the proceedings of TLCA'13 [pdf].
• Imperfect information in logic and concurrent games, with Julian Gutierrez and Glynn Winskel, to appear. [pdf (preliminary version)]
• 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.

Recent talks

• Talk at the University of Birmingham, untitled "Concurrent games with symmetry". [pdf]
• Talk at the PPS Seminar (Paris 7), untitled "Concurrent games with symmetry".
• Talk at the category theory seminar, Centre for Mathematical Science, Cambridge, untitled "Isomorphisms of types in the presence of higher-order references".
• Talk at LICS11 (22.06.11) in Toronto, untitled "Isomorphisms of types in the presence of higher-order references". [pdf]
• Talk at the 11th Wessex Theory Seminar (17.06.11) in Leicester, on isomorphisms of types in the presence of higher-order references.
• Talk at the department of Computer Science of the University of Oxford (14.06.11) on isomorphisms of types in the presence of higher-order references.
• Talk at TLCA11 (02.06.11) in Novi Sad, untitled "The Biequivalence of Locally Cartesian Closed Categories and Martin-Lof Type Theory". [pdf]
• Talk at the department of Computer Science of the University of Cambridge (06.05.11) on isomorphisms of types in the presence of higher-order references.
• Talk at FOSSACS11 (30.03.11) in Saabrücken, untitled "Estimation of the length of interactions in arena game semantics". [pdf]

Unpublished notes and reports

• 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]

Other stuff

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

Note importante

• La page de Stephane Zimmermann
• La page de Julien Cristau
• La page wiktionnaire sur 44