20 citations · 79 across the 14 of their papers we have counts for
18 papers
Extensional Taylor Expansion
Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair
We introduce a calculus of extensional resource terms. These are resource terms à la Ehrhard-Regnier, but in infinitely eta-long form. The calculus still retains a finite syntax an…
Strategies as Resource Terms, and their Categorical Semantics
Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair
As shown by Tsukada and Ong, simply-typed, normal and eta-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. The original pro…
The Cartesian Closed Bicategory of Thin Spans of Groupoids
Pierre Clairambault, Simon Forest
Recently, there has been growing interest in bicategorical models of programming languages, which are "proof-relevant" in the sense that they keep distinct account of execution tra…
The Mays and Musts of Concurrent Strategies
Simon Castellan, Pierre Clairambault, Glynn Winskel
Concurrent strategies based on event structures are examined from the viewpoint of 'may' and 'must' testing in traditional process calculi. In their pure form concurrent strategies…
The Quantitative Collapse of Concurrent Games with Symmetry
Pierre Clairambault, Hugo Paquet
We explore links between the thin concurrent games of Castellan, Clairambault and Winskel, and the weighted relational models of linear logic studied by Laird, Manzonetto, McCusker…
Positional Injectivity for Innocent Strategies
Lison Blondeau-Patissier, Pierre Clairambault
In asynchronous games, Melli{è}s proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insight…
Disentangling Parallelism and Interference in Game Semantics
Simon Castellan, Pierre Clairambault
Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to ha…
Learning to Count up to Symmetry
Pierre Clairambault
In this paper we develop the theory of how to count, in thin concurrent games, the configurations of a strategy witnessing that it reaches a certain configuration of the game. This…
Categories with Families: Unityped, Simply Typed, and Dependently Typed
Simon Castellan, Pierre Clairambault, Peter Dybjer
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we i…
Games and Strategies as Event Structures
Simon Castellan, Pierre Clairambault, Silvain Rideau +1
In 2011, Rideau and Winskel introduced concurrent games and strategies as event structures, generalizing prior work on causal formulations of games. In this paper we give a detaile…
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)
Simon Castellan, Pierre Clairambault, Peter Dybjer
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1 , Sigma-types, Pi-types, and a base type is a free category with familie…
Bounding linear head reduction and visible interaction through skeletons
Pierre Clairambault
In this paper, we study the complexity of execution in higher-order programming languages. Our study has two facets: on the one hand we give an upper bound to the length of interac…
Thin Games with Symmetry and Concurrent Hyland-Ong Games
Simon Castellan, Pierre Clairambault, Glynn Winskel
We build a cartesian closed category, called Cho, based on event structures. It allows an interpretation of higher-order stateful concurrent programs that is refined and precise: o…
Isomorphisms of types in the presence of higher-order references (extended version)
Pierre Clairambault
We investigate the problem of type isomorphisms in the presence of higher-order references. We first introduce a finitary programming language with sum types and higher-order refer…
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
Pierre Clairambault, Peter Dybjer
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categorie…
Isomorphisms of types in the presence of higher-order references
Pierre Clairambault
We investigate the problem of type isomorphisms in a programming language with higher-order references. We first recall the game-theoretic model of higher-order references by Abram…
Estimation of the length of interactions in arena game semantics
Pierre Clairambault
We estimate the maximal length of interactions between strategies in HO/N game semantics, in the spirit of the work by Schwichtenberg and Beckmann for the length of reduction in si…
Least and greatest fixpoints in game semantics
Pierre Clairambault
We show how solutions to many recursive arena equations can be computed in a natural way by allowing loops in arenas. We then equip arenas with winning functions and total winning…