The straightforward elimination of union types is known to break subject reduction, and for some extensions of the lambda-calculus, to break strong normalization as well. Similarly...
We introduce a Game Semantics where strategies are partial orders, and composition is a generalization of the merging of orders. Building on this, to bridge between Game Semantics ...
G¨odel’s completeness theorem is concerned with provability, while Girard’s theorem in ludics (as well as full completeness theorems in game semantics) are concerned with proo...
In this paper we solve an open problem posed in our previous work on asynchronous subtyping [12], extending the method to higher-order session communication and functions. Our syst...
Finiteness spaces constitute a categorical model of Linear Logic whose objects can be seen as linearly topologised spaces, (a class of topological vector spaces introduced by Lefsc...
Abstract. We investigate the question of what constitutes a proof when quantifiers and multiplicative units are both present. On the technical level this paper provides two new as...