Séminaire, Oct. 13, 2016
La rencontre aura lieu en amphi B, à l'ENS de Lyon.
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 SelfReferential 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 selfreferential. Instances of this scenario are higherorder calculi like the λcalculus, the calculus of higherorder communicating systems (CHOCS), the higherorder πcalculus (HOπ), HOcore, etc. It is well known that higherorder 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 selfreferential behaviour is still elusive.
We address these difficulties by providing an abstract characterisation of selfreferential behaviours as selfreferential 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 higherorder 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. higherorder process algebras): selfreferential endofunctors are shown to be universal among them. Universality renders selfreferential 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)
In intuitionistic realizability like Kleene's or Kreisel's, the axiom of choice is trivially realized. It is even provable in MartinL\"of's intuitionistic type theory. In classical logic, however, even the weaker axiom of countable choice proves the existence of noncomputable 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 coexist 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.