Disentangling Parallelism and Interference in Game Semantics

Autor: Simon Castellan, Pierre Clairambault

Publikováno v: Logical Methods in Computer Science, Vol Volume 20, Issue 3 (2024)

Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to have obtained full abstraction results for programming languages with a

Externí odkaz: https://doaj.org/article/65319b39c5e14e2ea1a61e1bb3852de7

Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)

Autor: Simon Castellan, Pierre Clairambault, Peter Dybjer

Publikováno v: Logical Methods in Computer Science, Vol Volume 13, Issue 4 (2017)

We show that a version of Martin-L\"of 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 families (supporting these type formers) both in a 1- and a 2-categorical s

Externí odkaz: https://doaj.org/article/b8cd19b82c994898896efc0f008019f3

Bounding linear head reduction and visible interaction through skeletons

Autor: Pierre Clairambault

Publikováno v: Logical Methods in Computer Science, Vol Volume 11, Issue 2 (2015)

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 interactions between bounded P-visible strategies in Hyland-Ong game semantic

Externí odkaz: https://doaj.org/article/9dfc5690da864f3ba4e04715819e0b84

The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding

Autor: Simon Castellan, Pierre Clairambault

Publikováno v: Proceedings of the ACM on Programming Languages. 7:689-717

We introduce a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. Our machine takes the shape of a compositional interpretation of terms as Petri structures, certai

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::00fad5f42311e81e537db6cf740856b5
https://doi.org/10.1145/3571217

Categories with Families: Unityped, Simply Typed, and Dependently Typed

Autor: Pierre Clairambault, Peter Dybjer, Simon Castellan

Publikováno v: Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics ISBN: 9783030665449
Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics
Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, 20, Springer International Publishing, pp.135-180, 2021, Outstanding Contributions to Logic, ⟨10.1007/978-3-030-66545-6_5⟩

We show how the categorical logic of the untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with families (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::59efd880a7ae4049c916671ae2fbfaa6
https://doi.org/10.1007/978-3-030-66545-6_5