Les séminaires sont communs avec l'équipe Plume (ENS Lyon) et ont lieu en salle de séminaire, premier étage du bâtiment Le Chablais, sur le site du Bourget du Lac ou à l'ENS Lyon.

Prochain séminaire :

Jeudi 02 juin 2016 à 10h Tingxiang Zou (Université Lyon 1),
Classical and relative realizability

Résumé : (Masquer les résumés)
Thomas Streicher has reformulated Krivine's notion of classical realizability into abstract Krivine structures and showed that from any such structure one can build a tripos out of it. They are called Krivine triposes and form a subclass of relative realizability triposes in the sense of van Oosten and Hofstra. In this talk, I will present a characterization of those Krivine triposes, indeed, they are exactly boolean subtriposes of relative realizability triposes. I will also talk about a concrete construction of non-localic Krivine triposes. These results are from my master thesis supervised by Jaap van Oosten.

Le séminaire de l’équipe LIMD est sous la responsabilité de Xavier Provençal.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, toutes ensemble.

Année 2016

Jeudi 15 septembre 2016 à 10h Ilias Garnier (ENS Paris),
À venir

Résumé : (Masquer les résumés)
À venir

Jeudi 16 juin 2016 à 10h Tomer Libal (École Polytechnique),
À venir

Résumé : (Masquer les résumés)
À venir

Jeudi 02 juin 2016 à 10h Tingxiang Zou (Université Lyon 1),
Classical and relative realizability

Résumé : (Masquer les résumés)
Thomas Streicher has reformulated Krivine's notion of classical realizability into abstract Krivine structures and showed that from any such structure one can build a tripos out of it. They are called Krivine triposes and form a subclass of relative realizability triposes in the sense of van Oosten and Hofstra. In this talk, I will present a characterization of those Krivine triposes, indeed, they are exactly boolean subtriposes of relative realizability triposes. I will also talk about a concrete construction of non-localic Krivine triposes. These results are from my master thesis supervised by Jaap van Oosten.

Jeudi 26 mai 2016 à 10h Frédéric Blanqui (INRIA),
Size-based termination for higher-order rewrite systems

Résumé : (Masquer les résumés)
At POPL'96, Hughes, Pareto and Sabry presented an approach to the termination of closed ML-like programs based on type-checking and the abstract interpretation of a semantic notion of size. This approach was then extended by several authors to open terms and more complex type systems. In the first part, I will show how it can be extended in other directions: arbitrary user-defined notions of size and rewriting-based function definitions. In the second part, I will show how the decidability of type-checking (with size-induced subtyping) can be reduced to the existence, in the size algebra, of a smallest solution for any solvable set of inequalities, and show it for the successor algebra (which is enough to subsume Coq termination checker for instance).

Jeudi 19 mai 2016 à 10h Matteo Mio (ENS Lyon),
Measure Quantifier in Monadic Second Order Logic

Résumé : (Masquer les résumés)
In this talk I will present some recent work, with H. Michalewski, on the study of an extension of MSO on infinite trees with the so-called ``measure quantifier''. This kind of research is motivated, as I will discuss, by a long-standing open problem in the field of verification of probabilistic programs. I will state a negative (i.e., undecidability) result but also present some interesting (currently) open problems.

Jeudi 14 avril 2016 à 10h Jean-Bernard Stefani (INRIA),
Location Graphs - A model for dynamic component systems

Résumé : (Masquer les résumés)
We introduce location graphs, a process calculus framework for modeling dynamic component systems. A key aspect of the framework is its ability to model different forms of component composition, dynamic component structures with sharing, and different forms of separation and encapsulation constraints. We present the operational semantics of the framework and hint at a type system for location graphs.

Jeudi 31 mars 2016 à 10h, 4-Canton-61 Federico Orsanigo (LAMA),
Concurrent processes and directed algebraic topology

Résumé : (Masquer les résumés)
Directed algebraic topology is a young subject which takes inspiration from homotopy theory and concurrent processes. Differently from algebraic topology, it studies situations in which paths are, in general, not invertible. For this reason directed algebraic topology is particularly suitable for modelling non-reversible phenomena like concurrent processes, where processes do not reverse. In this talk, based on [1], I start from concurrent processes and show how directed algebraic topology is a natural model for it. [1] Martin Raussen, ``Contributions to Directed Algebraic Topology: with inspirations from concurrency theory'', Doctoral Thesis, Department of Mathematical Sciences, Aalborg University.

Jeudi 24 mars 2016 à 10h Clovis Eberhart (LAMA),
Construire des terrains de jeux : catégories doubles fibrées

Résumé : (Masquer les résumés)
Les terrains de jeux sont des catégories double avec de la structure et des propriétés supplémentaires. Les quelques exemples de terrains de jeux connus s'appuient sur des constructions similaires. Je vais présenter une généralisation de cette construction de catégories double à partir de données plus simples que l'on appellera ``signature''. Moyennant certaines hypothèses sur la signature, on parvient à montrer une propriété cruciale des terrains de jeux : la propriété de fibration. On appliquera cette construction pour construire un terrain de jeux pour les jeux Hyland-Ong, et on comparera la structure obtenue aux structures classiques dans ces jeux.

Jeudi 18 février 2016 à 10h Durier Adrien (ENS Lyon),
Equations et contextes avec unicité des solutions dans les calculs de processus

Résumé : (Masquer les résumés)
Dans les calculs de processus (ccs, pi-calcul), les bisimulations modulos (up-to) sont des techniques de preuves utilisées pour montrer des équivalences entre processus [1]. Une méthode alternative, mais très similaire, consiste à montrer que deux processus sont solutions d'une même équation [2]. On présentera une telle technique reposant sur la non-divergence d'une solution minimale de l'équation, basée sur [3], qui illustre la correspondance entre bisimulations modulos et unicité des solutions, ainsi que les propriétés attendues d'un contexte dans un cadre abstrait (LTS). [1] Sangiorgi, Davide, and David Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge university press, 2003. [2] Sangiorgi, Davide. ``Equations, contractions, and unique solutions.'' POPL 2015. [3] Roscoe, A. W. ``Topology, computer science, and the mathematics of convergence.'' Topology and category theory in computer science. Oxford University Press, Inc., 1991.

Jeudi 28 janvier 2016 à 10h JB Stefani (à venir),
à venir

Résumé : (Masquer les résumés)
À venir

Jeudi 07 janvier 2016 à 10h Sebastián Barbieri (ENS Lyon),
A short proof of the existence of strongly aperiodic subshifts over {0,1} in countable groups

Résumé : (Masquer les résumés)
A Theorem of Gao, Jackson and Seward, originally conjectured to be false by Glasner and Uspenskij, asserts that every countable group admits a strongly aperiodic subshift over a 2-symbol alphabet. Their proof consists of a quite technical construction. We give a shorter proof of their result by using the asymetrical version of Lovasz Local Lemma which allows us also to prove that this subshift is effectively closed (with an oracle to the word problem of the group) in the case of a finitely generated group. This is about joint work with Nathalie Aubrun and Stéphan Thomassé.

Le séminaire de l’équipe LIMD est sous la responsabilité de Xavier Provençal.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, toutes ensemble.