The seminar of the team LIMD is under the responsibility of Xavier Provencal.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, all years together.

Year 2017

Thursday 22nd June 2017 at 10h Tom Hirschowitz (LAMA),
Categorical combinatorics of concurrent innocent strategies

Abstract: (Hide abstracts)
Game semantics is a class of denotational models for programming languages, in which types are interpreted as games and programs as strategies. In order to interpret pure programs, one has to restrict to innocent strategies. Two key results then entail that they are the morphisms of a category: associativity of composition and stability of innocence. These are non-trivial results, and significant work, notably by Melliès, has been devoted to better understanding them. Recently, games models have been extended to concurrent languages, using presheaves as generalised strategies and recasting innocence as a sheaf condition. We here revisit composition of strategies in concurrent game semantics with abstract categorical tools that make most of the reasoning automatic and extract the few crucial lemmas that give composition of strategies all its desired properties. The approach applies to non-concurrent strategies as well.

Thursday 1st June 2017 at 10h Karim Nour (LAMA),
Autour de la normalisation forte du lambda-calcul simplement typé

Abstract: (Hide abstracts)
Je présenterai plusieurs preuves de normalisation du lambda-calcul simplement typé avec une majoration de la longueur d'une normalisation d'un terme typé donné. J'expliquerai rapidement comment le dernier résultat se généralise au lambda-mu-calcul simplement typé. L'exposé est accessible à tous les membres de l'équipe.

Thursday 18th May 2017 at 10h Damiano Mazza (LIPN (Paris 13)),
Church Meets Cook and Levin

Abstract: (Hide abstracts)
The Cook-Levin theorem (the statement that SAT is NP-complete) is a central result in structural complexity theory. What would a proof of the Cook-Levin theorem look like if the reference model of computation were not Turing machines but the lambda-calculus? We will see that exploring the alternative universe of ``structural complexity with lambda-terms instead of Turing machines'' brings up a series of interesting questions, both technical and philosophical. Some of these have satisfactory answers, leading us in particular to a proof of the Cook-Levin theorem using tools of proof-theoretic and semantic origin (linear logic, Scott continuity), but many others are fully open, leaving us wondering about the interactions (or lack thereof) between complexity theory and proof theory/programming languages theory.

Monday 24th April 2017 at 10h Anurag Pandey (MPI),
Algebraic Independence of Polynomials over Fields of Positive Characteristic

Abstract: (Hide abstracts)
Two polynomials f and g are said to be algebraically dependent over a field K if there exists a non-zero bivariate polynomial A with coefficients in K such that A(f,g)=0. If no such polynomial exists, we say that f and g are independent. This is a natural generalization of linear independence to higher degrees. We consider the problem of finding an algorithm to test whether the given set of polynomials are algebraically independent. When the field has characteristic zero, this problem has a randomised polynomial time algorithm using the Jacobian Matrix of the given polynomials. However the criterion fails when the polynomials are taken over the fields of positive characteristic. One can expect that the positive characteristic case also has an efficient algorithm for testing algebraic independence, however, the existing best known upper bound is very far from desired. The talk will cover a result which is an attempt to bridge this gap. We present a new algorithm which is based on a refined generalisation of Jacobian criterion in case of fields of positive characteristic. It also yields a structural result about the algebraically dependent polynomials - approximate functional dependence.

Thursday 6th April 2017 at 10h Flavien Breuvart (Paris 13),
Un type est-il composé de termes ou un terme composé de types?

Abstract: (Hide abstracts)
S'il est commun, dans la communauté de réalisabilité, de considérer un type comme l'ensemble de ses preuves, et donc un ensemble de termes, il est aussi commun, dans la communauté des types intersections, de considérer un terme comme l'ensemble de ses comportements possibles, et donc un ensemble de types. Dans cet exposé, je présenterai en détail les types intersections, qui sont moins connus au sein du LAMA. Puis j'essaierai d'expliciter les liens avec la réalisabilité: en quoi il est intéressant de composer les deux, et si l'on peut voir les deux opérations comme duales dans un certain sens. Il ne s'agira pas (ou peu) de travaux personnels, mais d'une présentation générale et transversale du domaine.

Monday 27th March 2017 at 10h Manfred Madritsch (Nancy),
Systèmes dynamiques et l'équirépartition des suites

Abstract: (Hide abstracts)
Cet exposé considère l'amélioration de Furstenberg du théorème de récurrence de Poincare. Nous commençons avec ce théorème et faisons une connexion avec la théorie d'équirépartition des suites. Les rotations du cercle donnent des exemples élémentaires des suites équiréparties et des systèmes dynamique. En considèrent leur généralisations le théorème de van der Corput joue un rôle central et nous analysons ce théorème et ses conséquences. Le concept d'un ensemble de van der Corput boucle la boucle avec le théorème de Furstenberg-Sárközy.

C'est de travail conjoint avec Robert Tichy de l'Université Technique de Graz.

Thursday 16th March 2017 at 10h Lionel Nguyen Van Thé (Aix-Marseille Université),
Théorie de Ramsey structurale et dynamique topologique

Abstract: (Hide abstracts)
L'objet de la théorie de Ramsey est l'étude de l'apparition nécessaire de la régularité au sein des structures de grande taille, même lorsque ces dernières sont soumises à des partitions. Par exemple, le théorème de Ramsey affirme que tout graphe infini admet un sous-graphe induit complet (où tous les sommets sont reliés à tous les autres) ou indépendant (où aucun sommet n'est relié à aucun autre). De manière équivalente, pour toute partition finie de l'ensemble des paires de nombres naturels, il existe un ensemble infini de naturels dont les paires sont toutes dans la même partie. Un autre exemple est donné par le théorème de van der Waerden, qui affirme que pour toute partition des entiers naturels en un nombre fini de parties, l'une des parties contient nécessairement des progressions arithmétiques de longueur finie arbitrairement grande (il se peut en revanche qu'aucune des parties ne contienne de progression arithmétique infinie).

Le but de cet exposé sera de présenter dans quelle mesure des résultats de ce type peuvent être obtenus dans des contextes où plus de structure apparaît (espaces vectoriels, espaces métriques, graphes, graphes dirigés, etc), et de montrer comment, à partir des travaux de Kechris, Pestov et Todorcevic de 2005, ces résultats peuvent être utilisés pour démontrer des résultats de dynamique topologique, tels que le théorème suivant, dû à Pestov : Soit G le groupe d'automorphismes des rationnels (vus comme l'unique ordre total dense sans point d'extrémité). Alors, lorsqu'il est équipé de la topologie adéquate, G est extrêmement moyennable, c'est-à-dire que toute action continue de G par homéomorphismes sur un espace compact admet un point fixe.

Thursday 16th February 2017 at 10h Jean-Bernard Stefani (INRIA),
TBA

Abstract: (Hide abstracts)
TBA

Thursday 2nd February 2017 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 2nd February 2017 at 10h Andrea Frosini (Florence),
Reconstruction of 2-convex polyominoes

Abstract: (Hide abstracts)
A polyomino P is called 2-convex if for every two cells belonging to P, there exists a monotone path included in P with at most two changes of direction. We present some tomographical properties of 2-convex polyominoes from their horizontal and vertical projections and gives an algorithm that reconstructs them from a given couple of projections. We discuss its complexity.

Thursday 26th January 2017 at 10h Lama Tarsissi (LAMA),
Second order balance property on Christoffel words

Abstract: (Hide abstracts)
Balanced words have been studied a lot in the last decades. In particular, Christoffel words that are a special case of finite balanced words. In this talk, I introduce the Balance matrix that studies the balancedness of these words and I define some tools to extend this property by defining a second order of balancedness. I recall some properties about the continued fraction development and the Stern-Brocot tree to prove a recursive formula based on the shape of the path from the root of the Stern-Brocot. Finally, I show that among all infinite paths in the Stern-Brocot tree, the one that converges to φ, the golden ratio, minimizes the growth of the second order balance.

Thursday 19th January 2017 at 10h Pawel Sobocinski (Southampton),
Programming recurrence relations

Abstract: (Hide abstracts)
Recurrence relations have been of interest since ancient times. Perhaps the most famous is the Fibonacci numbers, where each additional term in the sequence is obtained as the sum of the previous two. I will show how we can use a graphical language of string diagrams–a “graphical linear algebra”–to reason about recurrence relations, and as a bonus, obtain efficient implementations. This application comes from a general string diagrammatic theory of signal flow graphs–a model of computation originally studied by Claude Shannon in the 1940s–developed in collaboration with Filippo Bonchi and Fabio Zanasi, and published at CONCUR 2014 and PoPL 2015.

The seminar of the team LIMD is under the responsibility of Xavier Provencal.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, all years together.