Go back to An-fang, the Peace Square at An-Fang, the Beginning Place at An-Fang, where
all things start (…) An-Fang was near a city, the only living city with a pre-atomic name (…) …

We present a game semantics for Linear Logic, in which formulas denote games and proofs
denote winning strategies. We show that our semantics yields a categorical model of Linear …

In the past s Li. e-ai years types have become an important component of programming iat;
guagc dcsigg. TZi< y pmvde a logical framework to ensure that programs meet given …

A polymorphic function is parametric if its behavior does not depend on the type at which it is
instantiated. Starting with Reynolds' work, the study of parametricity is typically semantic. In …

We propose that the phenomenon of local state may be understood in terms of Strachey's
concept of parametric (ie, uniform) polymorphism. The intuitive basis for our proposal is the …

Jean-Yves Girard and John Reynolds independently discovered the second-order
polymorphic lambda calculus, F2. Girard additionally proved a Representation Theorem …

In this paper, we present a Game Semantics for Linear Logic [Gir87], in which formulas
denote games, and proofs denote winning strategies. We also prove a novel kind of …

In this collection we try to give an overview of some selected topics in Domain Theory and
Denotational Semantics. In doing so, we rst survey the mathematical universes which have …

Sequentiality vs. concurrency in games and logic Page 1 Math. Struct. in Comp. Science (2003),
vol. 13, pp. 531–565. c 2003 Cambridge University Press DOI: 10.1017/S0960129503003980 …

We present the model construction technique called Linear Realizability. It consists in
building a category of Partial Equivalence Relations over a Linear Combinatory Algebra. We …