Tuesday 7. Sept

ion/Full-Completeness proofs of Game Semantics, we identify conditions on the adjoint model which guarantee the validity of a Decomposition Theorem. For morphisms which inhabit ML types, this theorem allows to recover the top level structure of the corresponding Bohm trees. The fine analysis of intuitionistic types in terms of linear types plays an essential role here. In order to build a "concrete" fully complete model, we focus on realizability models, based on Partial Equivalence Relations (PERs) over a Linear Combinatory Algebra (LCA). In fact, PER categories over LCAs can be seen to be linear, and to form adjoint models with their co-Klesli categories. Our concrete fully complete model is obtained via linear realizability on an LCA of partial involutions. This LCA arises as a special case of a general categorical construction, i.e. Abramsky's generalized version of Girard's Geometry of Interaction. Samson Abramsky : Process Realizability Realizability in its usual formulation..