Séminaire, 13 octobre 2016

Programme

10:30 – 12:00

Jim Laird (University of Bath)

Invited talk: Weighted Models for Computation and Communication

14:00 – 15:00

Marco Peressotti (Univ. of Udine)

Invited talk: Coalgebraic Semantics of Self-Referential Behaviours

We investigate the semantics of systems which can refer to themselves, e.g., by “passing around" systems of the same kind as values (hence potential observables). For this reason, we refer to these systems as self-referential. Instances of this scenario are higher-order calculi like the λ-calculus, the calculus of higher-order communicating systems (CHOCS), the higher-order π-calculus (HOπ), HOcore, etc. It is well known that higher-order systems pose unique challenges and are difficult to reason about. Many bisimulations and proof methods have been proposed also in recent works. This ongoing active effort points out that a definition of abstract self-referential behaviour is still elusive.

We address these difficulties by providing an abstract characterisation of self-referential behaviours as self-referential endofunctors, i.e. functors whose definition depends on their own final coalgebra. The construction of these functors is not trivial, since they must be defined at once with their own final coalgebra and due to the presence of both covariant and contravariant dependencies (e.g. arising from higher-order inputs). We provide such a construction.

Similarly defined endofunctors arise from considering as object systems (i.e., those which can be values) only certain subclasses of systems (usually via some syntactic restriction) or a syntactic representations (cf. higher-order process algebras): self-referential endofunctors are shown to be universal among them. Universality renders self-referential endofunctors a touchstone for similar behavioural functors and offers the mathematical structure for assessing soundness and completeness of other models via properties of the associated universal morphisms.

15:30 – 16:30

Valentin Blot (University of Bath)

Invited talk: Hybrid realizability for intuitionistic and classical choice

In intuitionistic realizability like Kleene's or Kreisel's, the axiom of choice is trivially realized. It is even provable in Martin-L\"of's intuitionistic type theory. In classical logic, however, even the weaker axiom of countable choice proves the existence of non-computable functions. This logical strength comes at the price of a complicated computational interpretation which involves strong recursion schemes like bar recursion. We take the best from both worlds and define a realizability model for arithmetic and the axiom of choice which encompasses both intuitionistic and classical reasoning. In this model two versions of the axiom of choice can co-exist in a single proof: intuitionistic choice and classical countable choice. We interpret intuitionistic choice efficiently, however its premise cannot come from classical reasoning. Conversely, our version of classical choice is valid in full classical logic, but it is restricted to the countable case and its realizer involves bar recursion. Having both versions allows us to obtain efficient extracted programs while keeping the provability strength of classical logic.