Abstract We show that the principal types of the closed terms of the affine fragment of λ-calculus, with respect to a simple type discipline, are structurally isomorphic to their interpretations, as partial involutions, in a natural Geometry of Interaction model à la Abramsky. This permits to explain in elementary terms the somewhat awkward notion of linear application arising in Geometry of Interaction, simply as the resolution between principal types using an alternate unification algorithm. As a consequence, we provide an answer, for the purely affine fragment, to the open problem raised by Abramsky of characterizing those partial involutions which are denotations of combinatory terms.

International audience

In 2005, S. Abramsky introduced various universal models of computation based on Affine Combinatory Logic, consisting of partial involutions over a suitable formal language of moves, in order to discuss reversible computation in a game-theoretic setting. We investigate Abramsky’s models from the point of view of the model theory of λ-calculus, focusing on the purely linear and affine fragments of Abramsky’s Combinatory Algebras. Our approach stems from realizing a structural analogy, which had not been hitherto pointed out in the literature, between the partial involution interpreting a combinator and the principal type of that term, with respect to a simple types discipline for λ-calculus. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction (GoI). Our approach provides immediately an answer to the open problem, raised by Abram- sky, of characterising those finitely describable partial involutions which are denotations of combinators, in the purely affine fragment. We prove also that the (purely) linear combinatory algebra of partial involutions is a (purely) linear λ-algebra, albeit not a combinatory model, while the (purely) affine combinatory algebra is not. In order to check the complex equations involved in the definition of affine λ-algebra, we implement in Erlang the compilation of λ-terms as involutions, and their execution.

The LF P Framework is an extension of the Harper–Honsell–Plotkin's Edinburgh Logical Framework LF with external predicates , hence the name Open Logical Framework . This is accomplished by defining lock type constructors , which are a sort of ⋄ -modality constructors , releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i . e . via introduction , elimination and equality rules . Using LF P , one can factor out the complexity of encoding specific features of logical systems, which would otherwise be awkwardly encoded in LF, e . g . side-conditions in the application of rules in Modal Logics, and sub-structural rules, as in non-commutative Linear Logic . The idea of LF P is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincaré Principle or Deduction Modulo . Indeed such paradigms can be adequately formalized in LF P . We investigate and characterize the meta-theoretical properties of the calculus underpinning LF P : strong normalization, confluence and subject reduction. This latter property holds under the assumption that the predicates are well-behaved , i . e . closed under weakening, permutation , substitution and reduction in the arguments. Moreover, we provide a canonical presentation of LF P , based on a suitable extension of the notion of βη - long normal form , allowing for smooth formulations of adequacy statements.

Joyal's categorical construction on (well-founded) Conway games and winning strategies provides a compact closed category, where tensor and linear implication are defined via Conway disjunctive sum (in combination with negation for linear implication). The equivalence induced on games by the morphisms coincides with the contextual closure of the equideterminacy relation w.r.t. the disjunctive sum. Recently, the above categorical construction has been generalized to non-wellfounded games. Here we investigate Joyal's construction for a different notion of sum, i.e. selective sum. While disjunctive sum reflects the interleaving semantics, selective sum accommodates a form of parallelism, by allowing the current player to move in different parts of the board simultaneously. We show that Joyal's categorical construction can be successfully extended to selective sum, when we consider alternating games, i.e. games where each position is marked as Left player (L) or Right player (R), that is only L or R can move from that position, R starts, and L/R positions strictly alternate. Alternating games typically arise in the context of Game Semantics. This category of well-founded games with selective sum is symmetric monoidal closed, and it induces exactly the equideterminacy relation. Generalizations to non-wellfounded games give linear categories, i.e. models of Linear Logic. Our game models, providing a certain level of parallelism, may be situated halfway between traditional sequential alternating game models and the concurrent game models by Abramsky and Mellies. We work in a context of coalgebraic games, whereby games are viewed as elements of a final coalgebra, and game operations are defined as final morphisms.

The aim of this work is to correlate two different approaches to the semantics of programming languages: game semantics and intersection type assignment systems (ITAS). Namely, we present an ITAS that provides the description of the semantic interpretation of a typed lambda calculus in a game model based on innocent strategies. Compared to the traditional ITAS used to describe the semantic interpretation in domain theoretic models, the ITAS presented in this paper has two main differences: the introduction of a notion of labelling on moves, and the omission of several rules, i.e. the subtyping rules and some structural rules.

We extend the coalgebraic account of specification and refinement of objects and classes in object-oriented programming given by Reichel and Jacobs to(generalised) binary methods. These are methods that take more than one parameter of a class type. Class types include products, sums and powerset type constructors. To allow for classconstructors, we model classes asbialgebras. We study and compare two solutions for modelling generalised binary methods, which use purely covariant functors. In the first solution, which applies when we already have a class implementation, we reduce the behaviour of a generalised binary method to that of a bunch of unary methods. These are obtained byfreezingthe types of the extra class parameters to constant types. If all parameter types arefinitary, thebisimilarity equivalenceinduced on objects by this model yields thegreatest congruencewith respect to method application. In the second solution, we treat binary methods asgraphsinstead of functions, thus turning contravariant occurrences in the functor into covariant ones. We show the existence offinal coalgebrasin both cases.

We propose a general theory of partial n-place operations based solely on the primitive notion of the application of a (possibly partial) operation to n objects. This theory is strongly selfdescriptive in that the fundamental manipulations of operations, that is, application, composition, abstraction, union, intersection and so on, are themselves internal operations. We give several applications of this theory, including implementations of partial n-ary λ-calculus, and other operation description languages. We investigate the issue of extensionality and give weakly extensional models of the theory.