Lundi 22 septembre 2014, amphithéâtre Alan Turing. Organisation : Jean Krivine.

Je ferai une présentation rallongée de l'article LICS du même nom. Il s'agit de donner une caractérisation, pour une classe importante de modèles du lambda-calcul non typé, de la pleine adéquation pour la normalisation de tête (i.e. pour H*). On montrera en effet qu'il est pour cela nécessaire et suffisant d'être hyperimmune. L'hyperimmunité est une notion que nous introduirons qui demande à ce que les comportements mal fondés du modèle ne soient pas capturables par des fonctions récursives.

Event structures is the traditional denotational semantics used for process algebra. A limitation of event structures is that it can only express a simple form of causality between the actions of a process. Pi calculus is a process algebra with name substitution and with a special operator that restricts the scope of a name. This leads to a more complicated causality relation. We will discuss some of the approaches and problems of a denotational semantics for pi processes and sketch a possible solution.

A proof of semantic normalisation is the composition of a soundness/adequacy and of a completeness/"escape" proof, typically with respect to a Kripke or realisability/reducibility model. As emphasised by the normalisation-by-evaluation approach, its computational content is the composition of a semantic interpretation function with a reification function. We shall investigate what happens when considering two-valued models, and in particular analyse the computational content of Henkin's proof of completeness.

La transformation logique dite « Dialectica », inventée par Gödel dans les années 30, permet d'enrichir la logique de départ, intuitioniste, en réalisant en sus des principes légèrement classiques. Hélas, la présentation qui en est faite habituellement fleure bon les écrits antiques des logiciens de la préhistoire de l'équivalence de Curry-Howard, malgré une description catégorique due à de Paiva à la fin des années 80.

Dans cet exposé, nous en donnerons une présentation moderne, et montrerons que, vue comme une transformation de programme, le contenu calculatoire de Dialectica s'exprime naturellement comme une manipulation de piles dans la machine de Krivine. Le pouvoir expressif résultant est cependant moins puissant que celui de callcc, permettant ainsi d'appliquer Dialectica à des systèmes plus riches comme une théorie des types dépendante telle que CIC.

Automata for unordered unranked trees are relevant for defining schemas and queries for data trees in Json or XML format. While the existing notions are well-investigated concerning expressiveness, they all lack a proper notion of determinism, which makes it difficult to distinguish subclasses of automata for which problems such as inclusion, equivalence, and minimization can be solved efficiently. In this paper, we propose and investigate different notions of ``horizontal determinism'', starting from automata for unranked trees in which the horizontal evaluation is performed by finite state automata. We show that a restriction to confluent horizontal evaluation leads to polynomial-time emptiness and universality, but still suffers from coNP-completeness of the emptiness of binary intersections. Finally, efficient algorithms can be obtained by imposing an order of horizontal evaluation globally for all automata in the class. Depending on the choice of the order, we obtain different classes of automata, each of which has the same expressiveness as Counting MSO.