20 juin 2019, 11:00 : Séminaire

Charles Grellois (LIS, Aix-Marseille), Sur la terminaison des programmes probabilistes récursifs d'ordre supérieur

Au cours des vingt dernières années, il y a eu beaucoup de progrès sur le model-checking des programmes probabilistes et des programmes fonctionnels, mais le model-checking des programmes qui sont à la fois fonctionnels et probabilistes n'a pas reçu d'intérêt, alors que de tels programmes commencent à émerger dans des langages de programmation comme Church ou Anglican. Nous avons donc travaillé sur ce problème, et avons introduit les schémas de récursion d'ordre supérieur probabilistes (PHORS) pour modéliser les programmes fonctionnels probabilistes. On peut également voir les PHORS comme des généralisations des chaînes de Markov récursives d'Etessami et de Yannakakis. Nous avons, dans cette première approche, considéré le problème de la terminaison probabiliste, qui équivaut à la question de l'accessibilité probabiliste. Nous avons montré que la question est indécidable dès l'ordre 2. Nous avons donné une caractérisation de la terminaison à l'aide de points fixes, et développé une méthode adéquate (mais peut-être incomplète) pour calculer de façon approximée la probabilité de terminaison d'un PHORS d'ordre 2.

Ce travail a été réalisé par Naoki Kobayashi, Ugo Dal Lago et Charles Grellois.

6 juin 2019

Séminaire Chocola à Lyon.

23 mai 2019, 11:00 : Séminaire

Aurore Alcolei (LIP, ÉNS Lyon & Computer Laboratory, Cambridge), Concurrent Games with side-information

Game semantics is an interactive denotational semantics: a denotation specifies the behaviour of a term/proof with respect to its environment. As such it is one of the most intensional model available in the Curry-Howard community.

Despite their intensional persprective, game models still omit a number of computational informations by hiding away internal reductions. This power of abstraction is at the core of the methodology of denotational semantics in that it aims to provide invariants under reduction. Yet, in some cases, this abstraction is too strong and prevents to capture some desirable informations.

In this talk, I will present how the model of concurrent game and strategies on event structures can be naturally extended with annotations from any (in)equational theory to keep track of side-information, that is information that may vary with interactions but does not influence their outcomes.

Depending on time and audience's interest, I will present this construction through two independent results: on the logic side I will show how this model instantiated with terms can be used to give a new interpretation and proof of the Herbrand's theorem; on the programming side I will introduce a semantics for R-IPA, a concurrent programming language with shared memory and an operational semantics keeping track of resource consumption, based on an instantiation of that same model with annotations being functions over reals.

9 mai 2019

Séminaire Chocola à Lyon.

25 avril 2019, 11:00 : Séminaire

Raphaëlle Crubillé (IRIF, Paris 7), Probabilistic Stable Functions on Discrete Cones are Power Series

The category of probabilistic coherence spaces (PCoh_!), introduced by Danos and Ehrhard, is a fully abstract model for PCF with discrete probabilities, where morphisms can be seen as power series. The category Cstab_m, of measurable cones and measurable stable functions, has been introduced by Ehrhard, Pagani and Tasson as a model for PCF with continuous probabilities.

In this talk, we will study the shape of stable functions when they are between discretecones: we will show that they can actually be seen as generalized power series. The proof is based on a generalization of a theorem from real analysis due to Bernstein, that states that all absolutely monotonous functions on reals are power series. From there, we will build a full and faithful functor from PCoh_! into Cstab_m that moreover preserves the cartesian closed structure.

4 avril 2019

Séminaire Chocola à Lyon.

21 mars 2019, 11:00 : Séminaire

Luigi Santocanale (LIS, Aix-Marseille), Quantales MIX *-autonomes et l'ordre faible continu

L'ensemble des permutations sur une ensemble fini possède la structure de treillis connue comme l'ordre faible de Bruhat. Cette structure s'étend aux mots sur un alphabet fini Σ = { x, y, z, . . . } tels que chaque lettre a un nombre fixé d'occurrences. Ces treillis sont connus comme "treillis multinomiaux" et, quand card(Σ) = 2, comme "treillis de chemins dans le réseau" (lattices of lattice path). Si on interprète les lettres x, y, z, . . . comme des axes, ces mots peuvent se voir comme des chemins discrets sur une grille dans un cube de dimension d = card(Σ).

Dans cet exposé j'expliquerai comment étendre cet ordre aux (images des) chemins continus croissants de l'intervalle [0,1] vers le cube [0,1]^d (qui préservent les extrémités 0 et 1). On obtient ainsi un treillis noté L_d([0,1]) ; l'outil clé de cette construction est le quantal (ou treillis résidué involutif) L_∨([0,1]) des fonctions sup-continues (cad, croissantes continue à gauche) de l'intervalle [0,1] vers lui même. Il s'agit d'un quantal (treillis résidué) cyclique *-autonome (involutif), qui satisfait la règle MIX.

Nous exposerons la structure des treillis L_d([0,1]) : ils sont auto-duaux, engendrés par sups par les éléments sup-irréductibles, il ne possèdent pas des éléments complétement sup-irréductibles. Quand d = 2, L_d([0,1]) = L_∨([0,1]) est la complétion de Dedekind-MacNeille des chemins discrets avec sauts rationnels. Quand d ≥ 3, cette propriété n'est plus vraie, mais chaque élément de L_d([0,1]) est un sup d'infs des chemins avec sauts rationnels.

14 mars 2019

Séminaire Chocola à Lyon.

28 février 2019, 11:00 : Séminaire

Claudia Faggian (IRIF, Paris 7), Lambda Calculus and Probabilistic Computation

In order to model higher-order probabilistic computation, a natural approach is to take the lambda calculus as a paradigm, and to enrich it with an operator which models probabilistic choice. The resulting calculus is however not confluent; such an issue is typically handled in the literature by fixing a deterministic reduction strategy.

Following [Plotkin75], we wish to preserve the key distinction between a calculus and a programming language. The former defines terms and reduction rules, and satisfy confluence, the latter is specified by a deterministic strategy (an abstract machine). Standardization is what relates the two: the programming language implements the standard strategy associated to the calculus. We propose two probabilistic lambda calculi, based respectively on the call-by-value and call-by-name parameter passing mechanism. The common root of the two calculi is a further calculus based on Linear Logic, which allows us to develop a unified, modular approach.

(joint work with Simona Ronchi Della Rocca)

24 janvier 2019

Séminaire Chocola à Lyon.

17 janvier 2019, 11:00 : Séminaire

Christophe Lucas (ÉNS Lyon), Towards a Proof Theory of the Riesz Modal Logic

It has recently been shown that two Riesz-modal-logic formulas are semantically equivalent if and only if they are equivalent when interpreted in all "modal Riesz spaces". In this talk we will introduce a hyper-sequent calculus for the theory of "modal lattice-ordered abelian groups" which builds on previous work fo Metcalfe, Olivetti and Gabbay. It is our hope to eventually extend this work to the theory of modal Riesz spaces.