The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2017, 2018, 2019, 2020, 2021, 2022, 2023, all years together.

Year 2016

Thursday 15th December 2016 at 10h Sébastien Tavenas (LAMA),
Bornes inférieures et supérieures en complexité arithmétique

Abstract: (Hide abstracts)
Ayant déjà parlé récemment de mes travaux de recherche dans un séminaire de l’équipe de géométrie, je propose, de les représenter en mettant plus l’accent sur mes travaux en complexité arithmétique. La question du temps de calcul nécessaire à l’évaluation des polynômes naturels semble fondamentale. Ainsi, quelle est la meilleure façon de calculer un polynôme f(X_1,…,X_n) à partir des opérations arithmétiques basiques + et *? En fait, certains polynômes sont difficiles à calculer. Par exemple, évaluer le permanent d'une matrice revient à compter le nombre de mariages parfaits dans un graphe. On commencera par une présentation de pistes de recherche actuelles en complexité arithmétique. Puis, on verra comment paralléliser ces calculs de manière efficace. Je présenterai mes derniers résultats : en particulier, je montrerai comment obtenir des bornes inférieures ``presque''-cubiques (et ainsi battre les bornes précédentes quadratiques) sur la taille des circuits arithmétiques de profondeur 3 calculant un polynôme donné. Enfin, je comptais juste montrer comment des conjectures de géométrie algébrique réelle impliquent des bornes inférieures non triviales pour le temps de calcul.

Monday 12th December 2016 at 14h Shigeki Akiyama (Tsukuba),
Rotational beta expansion and self-similar tilings

Abstract: (Hide abstracts)
We study a generalization of beta expansion to 2 dimension involving rotation action. Basic questions are its ergodicity and soficness. In particular, sofic cases give rise to a large class of self-similar polygonal tilings, having 2n-th fold (diffractive) symmetry for any n. This is a joint work with Jonathan Caalim.

Thursday 8th December 2016 at 10h Karim Nour (LAMA),
Un nouveau résultat de complétude du lambda-mu-calcul simplement typé pour une sémantique de réalisabilité

Abstract: (Hide abstracts)
Je présenterai une nouvelle sémantique de réalisabilité du lambda-mu-calcul simplement typé et je montrerai un résultat de correction pour la valider. Je donnerai ensuite un modèle particulier de ce calcul qui permettra de prouver la complétude. Je finirai par quelques conséquences de ce résultat ainsi que quelques questions ouvertes.

Thursday 24th November 2016 at 10h Damien Pous (ENS Lyon),
Coinduction all the way up

Abstract: (Hide abstracts)
We revisit coinductive proof principles from a lattice theoretic point of view. By associating to any monotone function a function which we call the companion, we give a new presentation of both Knaster-Tarski's seminal result, and of the more recent theory of enhancements of the coinductive proof method (up-to techniques). The resulting theory encompasses parametrised coinduction, as recently proposed by Hur et al., and second-order reasoning, i.e., the ability to reason coinductively about the enhancements themselves. It moreover resolves an historical peculiarity about up-to context techniques. Based on these results, we present an open-ended proof system allowing one to perform proofs on-the-fly and to neatly separate inductive and coinductive phases.

Thursday 10th November 2016 at 10h Christophe Raffalli (LAMA),
Realization of a weak ultrafilter axiom

Abstract: (Hide abstracts)
On va montrer comment programmer sur des streams avec l'axiome de l'ultrafiltre, qui en quelque sorte correspond à une forme limitée de programmation concurrente pour calculer un stream infini.

Thursday 27th October 2016 at 10h Anna Frid (Aix-Marseille Université),
Suites uniformément distribuées engendrées par des mots morphiques

Abstract: (Hide abstracts)
A tout mot infini w uniquement ergodique, considéré comme un élément d'un sous-shift, nous associons un nombre réel nu(w) entre 0 et 1 égal à la mesure de l'ensemble des mots inférieurs ou égal à w. Lopez et Narbel ont montré (2016) que si la complexité du mot est assez basse, le décalage de mots correspond à un échange d'intervalles pour ces nombres associés. Nous montrons que si le mot w est un point fixe d'un ``bon'' morphisme, et en particulier d'un morphisme binaire, alors nu(w) et les valeurs de nu pour tous les décalages de w peuvent être trouvés à l'aide d'un morphisme sur les nombres réels.

Thursday 6th October 2016 at 10h Laurent Condat (GIPSA-lab),
Variation totale discrète : une nouvelle définition et sa minimisation

Abstract: (Hide abstracts)
Une nouvelle définition, implicite, du champ de gradient d'une image discrète est proposée. L'opération de différentiation qui associe une image a son champ de gradient, défini sur une grille deux fois plus fine, est non linéaire, et peut être vue comme l'inverse de l'opération (linéaire) d'intégration. Alors, la variation totale d'une image est simplement la norme l1 de l'amplitude de son champ de gradient. Cette nouvelle définition de la variation totale donne des contours nets et possède de meilleures propriétés d'isotropie que la définition classique.

Thursday 29th September 2016 at 10h Pierre-Etienne Meunier (La Motte-Servolex),
TBA

Abstract: (Hide abstracts)
TBA

Thursday 15th September 2016 at 10h Ilias Garnier (ENS Paris),
Stochastic mechanics of graph rewriting

Abstract: (Hide abstracts)
I will present an algebraic approach to stochastic graph-rewriting. Rules are seen as particular elements of an algebra of “diagrams”: the diagram algebra D. Diagrams can be thought of as formal computational traces represented in partial time. They can be evaluated to normal diagrams (each corresponding to a rule) and generate an associative unital non-commutative algebra of rules: the rule algebra R. Evaluation becomes a morphism of unital associative algebras which maps general diagrams in D to normal ones in R. In this algebraic reformulation, usual distinctions between graph observables (real-valued maps on the set of graphs defined by counting subgraphs) and rules disappear. Actual graph-rewriting is recovered as a canonical representation of the rule algebra as linear operators over the vector space generated by (isomorphism classes of) finite graphs. This shift of point of view, away from its canonical representation to the rule algebra itself, has unexpected consequences. We find that natural variants of the evaluation morphism map give rise to concepts of graph transformations hitherto not considered. This is joint work with N. Behr and V. Danos.

Thursday 23rd June 2016 at 10h Guilhem Jaber (Université Paris 7),
SyTeCi: Symbolic, Temporal and Circular reasoning for automatic proofs of contextual equivalence

Abstract: (Hide abstracts)
Operational Techniques (Kripke Logical Relations and Environmental/Open/Parametric Bisimulations) have matured enough to become now formidable tools to prove contextual equivalence of effectful higher-order programs. However, it is not yet possible to automate such proofs -- the problem being of course in general undecidable. In this talks, we will see how to take the best of these techniques to design an automatic procedure which is able many non-trivial examples of equivalence, including most of the examples from the literature. The talk will describe the main ingredients of this method: - Symbolic reduction to evaluate of programs, - Transition systems of heap invariants, as used with Kripke Logical Relations, - Temporal logic to abstract over the control flow between the program and its environment, - Circular proofs to automate the reasoning over guarded recursive predicates.

Thursday 16th June 2016 at 10h Tomer Libal (Inria Saclay),
Functions-as-constructors Higher-order Unification

Abstract: (Hide abstracts)
Unification is a central operation in the construction of a range of computational logic systems based on first-order and higher-order logics. First-order unification has a number of properties that dominates the way it is incorporated within such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respected the basic laws governing λ-binding (the equalities of α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been popular in various implemented systems and in various theoretical consideration, it is too weak for a number of applications. In this paper, we define an extension of pattern unification that is motivated by some existing applications and which satisfies these three properties. The main idea behind this extension is that the arguments to a higher-order, free variables can be more than just distinct bound variables: they can also be terms constructed from (sufficient numbers of) such variables using term constructor and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.

Thursday 2nd June 2016 at 10h Tingxiang Zou (Université Lyon 1),
Classical and relative realizability

Abstract: (Hide abstracts)
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.

Thursday 26th May 2016 at 10h Frédéric Blanqui (INRIA),
Size-based termination for higher-order rewrite systems

Abstract: (Hide abstracts)
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).

Thursday 19th May 2016 at 10h Matteo Mio (ENS Lyon),
Measure Quantifier in Monadic Second Order Logic

Abstract: (Hide abstracts)
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.

Thursday 14th April 2016 at 10h Jean-Bernard Stefani (INRIA),
Location Graphs - A model for dynamic component systems

Abstract: (Hide abstracts)
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.

Thursday 31st March 2016 at 10h Federico Orsanigo (LAMA),
Concurrent processes and directed algebraic topology

Abstract: (Hide abstracts)
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.

Thursday 24th March 2016 at 10h Clovis Eberhart (LAMA),
Construire des terrains de jeux : catégories doubles fibrées

Abstract: (Hide abstracts)
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.

Thursday 18th February 2016 at 10h Durier Adrien (ENS Lyon),
Equations et contextes avec unicité des solutions dans les calculs de processus

Abstract: (Hide abstracts)
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.

Tuesday 2nd February 2016 at 14h Anupam Das (ENS Lyon),
Monotonicity in Logic and Complexity

Abstract: (Hide abstracts)
Monotonicity is a fundamental notion in mathematics and computation. For usual real-valued functions R → R this simply corresponds to the notion that a function is increasing (or decreasing) in its argument, however this can be parametrised by any partially ordered domain and codomain we wish. In computation we deal with programs that compute Boolean functions, {0,1}* → {0,1}*. Restricting to increasing functions over this structure can be seen as prohibiting the use of negation in a program; for instance monotone Boolean functions are computed by Boolean circuits without NOT gates. The idea of restricting negation scales to other models of computation, and for some important classes of functions the formulation is naturally robust, not depending on the particular model at hand, e.g. for the polynomial-time functions. Monotone computational problems abound in practice, e.g. sorting a string and detecting cliques in graphs, and 'nonuniform' monotone models of computation, such as monotone circuits, have been fundamental objects of study in computational complexity for decades.

In this talk I will propose a project that develops *logical* characterisations of monotone complexity classes, via a proof theoretic approach. Namely, the project will identify theories of arithmetic whose formally representable functions coincide with certain monotone classes, and also develop fundamental recursion-theoretic programming languages in which to extract the monotone functions themselves. In particular the project focusses on the role of structural proof theory, i.e. the duplication and erasure of formulae, in controlling monotonicity.

Thursday 28th January 2016 at 10h JB Stefani (à venir),
à venir

Abstract: (Hide abstracts)
À venir

Thursday 7th January 2016 at 10h Sebastián Barbieri (ENS Lyon),
A short proof of the existence of strongly aperiodic subshifts over {0,1} in countable groups

Abstract: (Hide abstracts)
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é.

Seminars of team LIMD

Year 2016