The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
By year: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018.

Thursday 17th May 2018 at 10h Séminaire Chocola (ENS Lyon),

Thursday 5th April 2018 at 10h Séminaire Chocola (ENS Lyon),

Thursday 15th March 2018 at 10h Séminaire Chocola (ENS Lyon),

Thursday 8th February 2018 at 10h Séminaire Chocola (ENS Lyon),

Abstract: (Hide abstracts)

Thursday 1st February 2018 at 10h Thomas Rubiano (LIPN, Paris 13),
Implicit Computational Complexity meets Compilers

Abstract: (Hide abstracts)
Complexity theory helps us predict and control resources, usually time and space, consumed by programs. Static analysis on specific syntactic criterion allows us to categorize some programs. A common approach is to observe the program’s data’s behavior. For instance, the detection of non-size-increasing programs is based on a simple principle : counting memory allocation and deallocation, particularly in loops. This way, we can detect programs which compute within a constant amount of space. This method can easily be expressed as property on control flow graphs. Because analyses on data's behaviour are syntactic, they can be done at compile time. Because they are only static, those analyses are not always computable or easily computable and approximations need are needed. ``Size-Change Principle'' from C. S. Lee, N. D. Jones et A. M. Ben-Amram presented a method to predict termination by observing resources evolution and a lot of research came from this theory. Until now, these implicit complexity theories were essentially applied on more or less toy languages. This thesis applies implicit computational complexity methods into ``real life'' programs by manipulating intermediate representation languages in compilers. This give an accurate idea of the actual expressivity of these analyses and show that implicit computational complexity and compilers communities can fuel each other fruitfully. As we show in this thesis, the methods developed are quite generals and open the way to several new applications.

Thursday 25th January 2018 at 10h Youssef Fares (Amiens),
Autour de la conjecture de Poonen sur les polynômes quadratiques

Abstract: (Hide abstracts)
Soit c un nombre rationnel. Considérons le polynôme φ(X) = X^2 - c. On s’intéressse aux cycles de φ dans Q. Plus précisément, on s’intéresse à l’une des conjectures de Poonen selon laquelle tout cycle de φ dans Q admet une longueur au plus égale à 3. Dans notre exposé, on discutera de cette conjecture et on rappellera les résultats connus. En suite, on utilisera des moyens arithmetiques, combinatoriaux et analytiques simples pour étudier des cas particuliers de ce problème. Les outils utilisés dans cet exposé sont accessibles aux étudiants de master 2.

Thursday 14th December 2017 at 10h Séminaire Chocola (TBA),

Thursday 7th December 2017 at 10h Marie Kerjean (IRIF (Paris 7)),
Smooth models of linear logic

Abstract: (Hide abstracts)
La logique linéaire différentielle (DiLL) a été construite après une étude de modèles vectoriels de la logique linéaire, où les preuves sont interprétées par des séries plus ou moins formelles. Il s'agit donc de modèles discrets, où la différentielle extrait la partie linéaire d'une série entière. On cherche à trouver un modèle continu de la logique linéaire différentielle classique : il nous faut à la fois une catégorie cartésienne close de fonctions lisses et une catégorie monoidale close d'espaces réfléxifs. Nous allons détailler une solution partielle à ce problème, à travers d'espaces nucléaires et d'espaces de distributions. Nous verrons comment ce modèle suggère une syntaxe séparée en classes de formules, chaque classe correspondant aux solutions d'une EDP linéaire. Nous montrerons que chaque classe liée à une EDP dont on peut construire la solution se comporte comme une exponentielle intermédiaire, et vérifie les règles exponentielles de la logique linéaire différentielle. Si le temps le permet, nous aborderons un travail en collaboration avec Y. Dabrowski , où nous trouvons plusieurs modèles lisses de la logique linéaire différentielle, en faisant le choix discriminant d'interpréter la disjonction multiplicative de LL par le produit epsilon de Schwartz.

Thursday 30th November 2017 at 10h Clément Jacq (IRIF (Paris 7)),
Categorical combinatorics of non-deterministic innocent strategies

Abstract: (Hide abstracts)
In the first part of this talk, I'll recall the construction of category of games and innocent deterministic strategies introduced by Harmer, Hyland and Mellies [1]. Compared with the original method by Hyland and Ong [2], this method holds two specific advantages. First, it outlines the structural conditions on certain games and strategies by introducing separate entities (the schedules) that focus most of the required proof work. Second, the methods lays out a pretty clear combinatorial ‘recipe’ that could be replicated in other settings. That will be the goal of the second part of the talk, which will develop a 2-categorical and sheaf-theoretic formulation of non-deterministic innocent strategies, based on this ‘recipe’. During the course of this construction, I'll outline specific properties that give us a better understanding of both deterministic and non-deterministic strategies.

[1] Categorical combinatorics of innocent strategies, Harmer, Hyland, Mellies, LiCS 2007.
[2] On full abstraction for PCF I, II and III, Hyland, Ong, Information and Computation 2000.

Thursday 23rd November 2017 at 10h Giulio Manzonetto (Paris 13),
Refutation of Sallé's Longstanding Conjecture

Abstract: (Hide abstracts)
The lambda-calculus possesses a strong notion of extensionality, called ``the omega-rule'', which has been the subject of many investigations. It is a longstanding open problem whether the equivalence obtained by closing the theory of Böhm trees under the omega-rule is strictly included in Morris's original observational theory, as conjectured by Sallé in the seventies. We will first show that Morris's theory satisfies the omega-rule. We will then demonstrate that the two aforementioned theories actually coincide, thus disproving Sallé's conjecture.

The proof technique we develop is general enough to provide as a byproduct a new characterization, based on bounded eta-expansions, of the least extensional equality between Böhm trees.

Thursday 9th November 2017 at 10h Séminaire Chocola (TBA),

Thursday 19th October 2017 at 10h Aurore Alcolei (ENS Lyon),
The true concurrency of Herbrand's theorem

Abstract: (Hide abstracts)
Herbrand's theorem, widely regarded as a cornerstone of proof theory, exposes some of the constructive content of classical logic. In its simplest form, it reduces the validity of a first-order purely existential formula to that of a finite disjunction. More generally, it gives a reduction of first-order validity to propositional validity, by understanding the structure of the assignment of first-order terms to existential quantifiers, and the causal dependency between quantifiers. In this paper, we show that Herbrand's theorem in its general form can be elegantly stated as a theorem in the framework of concurrent games. The causal structure of concurrent strategies, paired with annotations by first-order terms, is used to specify the dependency between quantifiers. Furthermore concurrent strategies can be composed, yielding a compositional proof of Herbrand's theorem, simply by interpreting classical sequent proofs in a well-chosen denotational model.

Thursday 12th October 2017 at 10h Séminaire Chocola (TBA),

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),

Abstract: (Hide abstracts)

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.

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),

Abstract: (Hide abstracts)

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é.

Thursday 17th December 2015 at 10h Robert Bonnet (LAMA),
Caractérisation des espaces héréditairement ordonnables

Abstract: (Hide abstracts)
Travail en collaboration avec Arkady Leiderman, Ben Gurion University, Beer-Sheva, Israel. Un espace topologique $L$ est un espace ordonnable lorsqu'il existe un ordre total $leq$ sur $L$ tel que la topologie sur $L$ est engendrée par les intervalles ouverts (non nécessairement bornés) à extrémités dans $L$ (exemples: $N$, $Z$, $Q$, $R$; contre-exemple: $C$). Un espace $L$ est un espace héréditairement ordonnable si toute image continue de $L$ est ordonnable. On montre le résultat suivant: Si $L$ est un espace héréditairement ordonnable alors $L$ est un espace dénombrable et compact (i.e. un sous-espace compact de $R$, qui est donc homéomorphe a un ordinal dénombrable ayant un plus grand élément). En fait on montre un résultat plus général.

Thursday 10th December 2015 at 10h15 Jurriaan Rot (ENS Lyon),
Up-to techniques for bisimulations with silent moves

Abstract: (Hide abstracts)
Bisimulation is used in concurrency theory as a proof method for establishing behavioural equivalence of processes. Up-to techniques are a means of enhancing this proof method. In this talk I will argue that up-to techniques can be of general use, and discuss how this is supported by our coalgebraic framework of up-to techniques, that provides enhanced proof techniques for a wide variety of systems and a wide variety of properties. I will discuss our recent work on extending this framework to cover equivalences for systems that involve silent transitions.

Thursday 26th November 2015 at 10h Ilias Garnier (ENS Paris),
Le processus de Dirichlet comme transformation naturelle

Abstract: (Hide abstracts)
Le traitement catégorique de la théorie des probabilités formulé par Giry et Lawvere, basé sur la monade de probabilité G, permet de manipuler de façon élégante des probabilités d'ordre supérieur. Dans ce cadre, je présenterai une reconstruction du processus de Dirichlet, un objet largement utilisé en inférence bayésienne. Ce processus prend la forme d'une famille de mesures dans GG(X) indexée par M(X), où X est un espace Polonais et M(X) est l'espace des mesures finies non-zéro sur X. Sa construction repose sur deux outils dont l’intérêt dépasse le simple cas de la construction de Dirichlet. Le premier de ces outils est une version fonctorielle du théorème d'extension de Bochner adapté au cadre Polonais, qui permet d'étendre une famille projective de probabilités en une probabilité limite. Le second outil est une méthode de ``décomposition'' qui associe à tout espace Polonais zéro-dimensionnel une famille projective d'espaces finis, dont la limite projective est une compactification de l'espace originel. La combinaison de ces deux outils avec des propriétés bien connues de Dirichlet sur les espaces finis nous permet de reconstruire Dirichlet comme une transformation naturelle de M vers GG. Cette construction améliore les précédentes en ce qu'elle prouve la continuité de Dirichlet en ses paramètres.

Thursday 19th November 2015 at 10h Rodolphe Lepigre (Université Savoie Mont Blanc),
Un modèle de réalisabilité par valeur pour PML

Abstract: (Hide abstracts)
PML est un langage de programmation en appel par valeurs similaire à ML, avec une syntaxe à la Curry (c'est à dire, pas de types dans les termes) et basé sur une logique d'ordre supérieur classique. Les termes apparaissent dans les types via un prédicat d'appartenance t ∈ A et un opérateur de restriction A | t ≡ u. La sémantique de ces deux constructeurs de types utilise une relation d'équivalence (observationnelle) sur les programmes (non typés). L'opérateur de restriction est utile pour l'écriture de spécifications tandis que l'appartenance permet d'encoder les types dépendants. La présence de l'équivalence nous permet également de relâcher la « value restriction » pour obtenir un type produit dépendant compatible avec la logique classique (ce qui n'avait pas été fait avant).

Thursday 22nd October 2015 at 10h Pierre Hyvernat (LAMA),
Types inductifs et coinductifs, définitions récursives et ``size-change principle``

Abstract: (Hide abstracts)
Le ``size-change principle'' (SCP) est un algorithme simple donnant un test partiel de terminaison qui s'adapte très bien aux langages fonctionnels où les fonctions sont définies de manière récursive par pattern-matching. En présence de constructeurs paresseux, le SCP donne également un test (partiel) de productivité : c'est sur ce principe que les tests (terminaison + productivité) de PML et Agda reposent. Malheureusement, en présence de type coinductifs, certaines définitions récursives bien typées terminent (i.e. sont productives) mais sont incorrectes et rendent Agda/PML inconsistants. En utilisant les travaux de L. Santocanale sur les preuves circulaires et les jeux de parité, je montrerais comment utiliser le SCP pour implanter un test partiel de totalité des définitions récursives qui généralise le test de terminaison/productivité, et garantie qu'une définition est correcte vis à vis de son type.

Thursday 15th October 2015 at 10h Oscar Carrillo (LAMA),
Vérification formelle et incrémentale de spécifications SysML pour la conception de systèmes à base de composants

Abstract: (Hide abstracts)
Le travail à présenter est une contribution à la spécification et la vérification des Systèmes à Base de Composants (SBC) modélisés avec le langage SysML. Les SBC sont largement utilisés dans le domaine industriel et ils sont construits en assemblant différents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coût de développement. Malgré le succès de l’utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en œuvre d’approches plus rigoureuses. Dans ce contexte, nous allons traiter principalement deux problématiques: La première est liée à la difficulté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle est la suivante : comment spécifier une architecture SBC qui satisfait toutes les exigences du système ? Nous proposons une approche de vérification formelle incrémentale basée sur des modèles SysML et des automates d’interface pour guider, par les exigences, le concepteur SBC afin de définir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le Model Checker SPIN et la LTL pour spécifier et vérifier les exigences. La deuxième problématique traitée concerne le développement par raffinement d’un SBC modélisé uniquement par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu’une composition d’un ensemble de composants élémentaires et réutilisables raffine une spécification abstraite d’un SBC. Dans cette contribution, nous exploitons les outils : Ptolemy pour la vérification de la compatibilité des composants assemblés, et l’outil MIO pour la vérification du raffinement.

Thursday 17th September 2015 at 10h Christophe Raffalli (LAMA),
Tout faire avec le sous-typage

Thursday 3rd September 2015 at 10h Thomas Caissard (LIRIS),
Geodesic Distance and Metrics on Digital Surface

Abstract: (Hide abstracts)
The M2Disco (Multiresolution, Discrete and Combinatorial Models) research team aims at proposing new combinatorial, discrete and multiresolution models to analyse and manage various types of data such as images, 3D volumes and 3D meshes, represented as Digital Sur- faces (ie subset of Zn). One of their project called PALSE foam requires the computation of the shortest path between two points on a manifold. We are proposing the study of two algorithm for computing such a dis- tance, but also providing metric embedding inside a Discrete Exterior Calculus structure (DEC). We performs various tests regarding the two algorithms, but also con rm through experience DEC's operators con- vergence using suitable metric. This work is the base of both a research project named CoMeDiC (Convergent Metrics for Digital Calculus) and Ph.D. project.

Thursday 18th June 2015 at 10h Blanche Buet (Université Lyon 1),
Approximation de surfaces par des varifolds discrets

Abstract: (Hide abstracts)
Il existe de très nombreuses façons de représenter et discrétiser une courbe ou une surface, en raison notamment des applications envisagées et des modes d'acquisitions des données (nuages de points, approximations volumiques, triangulations...). Le but de cet exposé sera de présenter un cadre commun pour l'approximation des surfaces, dans l'esprit de la théorie géométrique de la mesure, à travers la notion de varifold discret. Ce cadre nous a notamment permis de dégager une notion de courbure moyenne discrète (à une échelle donnée) unifiée dont on présentera les propriétés de convergence et qu'on illustrera numériquement sur des nuages de points.

Thursday 4th June 2015 at 10h Svetlana Puzynina (Sobolev Institute of Mathematics et ENS Lyon),
Infinite self-shuffling words

Abstract: (Hide abstracts)
In this talk we introduce and study a new property of infinite words: An infinite word x on an alphabet A is said to be it self-shuffling, if x admits factorizations: $x=prod_{i=1}^infty U_iV_i=prod_{i=1}^infty U_i=prod_{i=1}^infty V_i$ with $U_i,V_i in A^*$. In other words, there exists a shuffle of x with itself which reproduces x. This property of infinite words is shown to be an intrinsic property of the word and not of its language (set of factors). For instance, every aperiodic uniformly recurrent word contains a non self-shuffling word in its shift orbit closure. On the other hand, we build an infinite word such that no word in its shift orbit closure is self-shuffling. We prove that many important and well studied words are self-shuffling: This includes the Thue-Morse word and all Sturmian words (except those of the form aC where a ∈ {0,1} and C is a characteristic Sturmian word). We further establish a number of necessary conditions for a word to be self-shuffling, and show that certain other important words (including the paper-folding word and infinite Lyndon words) are not self-shuffling. One important feature of self-shuffling words is its morphic invariance: The morphic image of a self-shuffling word is again self-shuffling. This provides a useful tool for showing that one word is not the morphic image of another. In addition to its morphic invariance, this new notion has other unexpected applications: For instance, as a consequence of our characterization of self-shuffling Sturmian words, we recover a number theoretic result, originally due to Yasutomi, on a classification of pure morphic Sturmian words in the orbit of the characteristic. Finally, we provide a positive answer to a recent question by T. Harju whether square-free self-shuffling words exist and discuss self-shufflings in a shift orbit closure. E. Charlier, T. Kamae, S. Puzynina, L. Q. Zamboni: Infinite self-shuffling words. J. Comb. Theory, Ser. A 128: 1-40 (2014) M. Müller, S. Puzynina, M. Rao: On Shuffling of Infinite Square-Free Words. Electr. J. Comb. 22(1): P1.55 (2015)

Thursday 28th May 2015 at 10h Colin Riba (ENS Lyon),
Fibrations of Tree Automata

Abstract: (Hide abstracts)
We propose a notion of morphisms between tree automata based on game semantics. Morphisms are winning strategies on a synchronous restriction of the linear implication between acceptance games. This leads to split indexed categories, with substitution based on a suitable notion of synchronous tree function. By restricting to tree functions issued from maps on alphabets, this gives a fibration of tree automata. We then discuss the (fibrewise) monoidal structure issued from the synchronous product of automata. We also discuss how a variant of the usual projection operation on automata leads to an existential quantification in the fibered sense. Our notion of morphism is correct, in the sense that it respects language inclusion, and in a weaker sense also complete.

Thursday 21st May 2015 at 10h30 Miquey Charguéraud et Salibra (Paris 7, Inria et Venise),
Séminaire Chocola

Thursday 7th May 2015 at 10h Hachem Hichri (Institut préparatoire aux études d’ingénieurs de Monastir),
Quelques résultats sur les nombres de Salem, les nombres de Pisot et les beta-nombres

Abstract available as a PDF file.

Thursday 30th April 2015 at 10h Emmanuel Beffara (Université d'Aix-Marseille),
Vers l'unification des systèmes de types pour processus mobiles

Abstract: (Hide abstracts)
Ce travail présente un cadre unificateur pour les systèmes de types pour les algèbres de processus. Le cœur du système fournit une correspondance précise entre des processus essentiellement fonctionnels et des démonstrations de logique linéaire; des fragments de ce système correspondent à des connections précédemment connues entre démonstrations et processus. On montre que l'ajout d'axiomes logiques peut étendre la classe des processus typables en échange de la perte de propriétés calculatoires comme l'absence de blocage ou la terminaison, ce qui permet de voir différents systèmes connus (types i/o, linéarité, contrôle) comme des instances d'un modèle général. Cette approche suggère des méthodes unifiées pour l'extension de systèmes de types avec de nouvelles propriétés tout en restant dans un cadre bien structuré, ce qui constitue un pas vers l'étude de la sémantique dénotationnelle des processus par des méthodes de théorie de la démonstration.

Thursday 23rd April 2015 at 10h Nadia Lafrenière (UQAM et LAMA),
La bibliothèque de Tsetlin : Diverses approches pour les marches aléatoires sur les permutations

Abstract: (Hide abstracts)
Dans cet exposé, nous étudierons différentes modélisations pour le mélange d'objets alignés (des livres, des cartes, des fichiers, etc.). En particulier, l'action qui correspond à piger un élément au hasard et à le remettre au début de la liste s'avère être un point de départ intéressant pour l'étude des marches aléatoires sur le groupe symétrique. Nous verrons que l'utilisation de techniques algébriques permet l'analyse de mélanges élaborés.

Thursday 9th April 2015 at 10h30 TBA (TBA),
Séminaire Chocola

Thursday 9th April 2015 at 10h Robert French (Université de Bourgogne),
Définition probabiliste d'un segment de droite discrète et automates cellulaires

Abstract: (Hide abstracts)
Cette présentation montrera un lien théorique entre les segments de droite discrète (DSS) et la théorie probabiliste des chemins possibles. Un DSS entre deux points est généralement défini comme la meilleure approximation discrète de la droite continue sous-jacente entre les deux points. Dans cet article, nous introduisons une autre définition qui fait écho à des approches dites de tous les chemins possibles de la physique des particules. Le cosmologiste George Ellis a récemment fait remarquer, ``Une particule prend tous les chemins qu'elle peut, et ce que nous voyons est la moyenne pondérée de toutes ces possibilités.'' Dans une veine similaire, nous définissons un segment de droite discrète entre deux points comme l'ensemble de pixels le plus rapproché de la moyenne pondérée de tous les chemins discrets possibles de longueur minimale entre les deux points. Cette définition est uniquement destinée à démontrer une relation théorique entre la théorie probabiliste des chemins discrets possibles et les DSSs. Elle n’a pas vocation à remplacer l’algorithme standard de Bresenham (1963) comme moyen pratique pour tracer les segments de droite dans le plan, mais de le justifier par une autre approche. Nous présentons également brièvement l’extension de cette définition dans l’espace à 3 dimensions. Nous présenterons également un nouvel algorithme récursif pour tracer un type de DSS présentant une meilleure autosimilarité que la DSS standard et qui est plus rapide que l'algorithme classique de Bresenham. Pour finir, nous implémenterons l’algorithme de tous les chemins possibles au moyen des automates cellulaires que nous appelons «Mants» (M-fourmis équipées de mémoires mais non réalistes). Il s’avère que le chemin qui est localement le plus probable entre la ``manthill'' et une source d'alimentation pour un individu de la colonie n’est, en général, pas identique à la trajectoire optimale pour la colonie dans son ensemble.

Thursday 2nd April 2015 at 14h Tom Hirschowitz (LAMA),
Analytic functors on presheaf categories (travail en cours avec Richard Garner, Macquarie Uni, Sydney)

Abstract: (Hide abstracts)
In denotational semantics, we have a few examples of notions which are easy to describe graphically (and generally informally), but whose algebraic axiomatisation is tedious, to say the least. Such examples include (in order of appearance) Lambek's polycategories, Girard's proof nets, and Lafont's interaction nets. The importance of algebraic axiomatisation of course resides in the induced notion of denotational model. In this work, we propose a generalisation of Joyal's analytic functors to certain presheaf categories, which we then use to directly derive algebraic axiomatisations from elementary graphical information. For concreteness, we instantiate our results on polycategories. The idea is that the pictures generally used to describe the standard operations on polycategories may be understood as a straightforward collection of finite presheaves on a certain category. Our notion of analytic functor then allows us to interpret this collection as an endofunctor on presheaves, which then freely generates a certain monad, whose algebras are precisely polycategories.

Thursday 26th March 2015 at 10h Pawel Gladki (Uniwersytet Śląski),
Hyperfields and their applications to Witt equivalence

Abstract: (Hide abstracts)
In this talk we shall recall the notion of hyperfields, i.e. fields with multivalued addition, provide a collection of examples of hyperfields, and show how they can be used to characterize Witt equivalence of fields. We shall also investigate the Witt equivalence of certain types of fields in some more detail.

Thursday 12th March 2015 at 10h30 TBA (TBA),
Séminaire Chocola

Thursday 5th March 2015 at 10h Rodolphe Lepigre et Christophe Raffalli (LAMA),
Mêler combinateurs, continuations et EBNF pour une analyse syntaxique efficace en OCaml

Abstract: (Hide abstracts)
Partie I (Rodolphe Lepigre) : Le développement de Patoline (un nouveau système de composition de documents) nécessite un parseur extensible d'OCaml sans contrainte, notamment sur l'analyse lexicale. Nous présentons ici un environnement de développement léger pour l'analyse syntaxique, conçu en deux mois pendant l'été 2014 pour répondre à ce besoin. Le système propose une syntaxe intuitive de type BNF, sans récursion à gauche. Les parseurs sont traduits vers des expressions OCaml utilisant DeCaP, notre bibliothèque de combinateurs monadiques, et sont donc des expressions de première classe. Pour optimiser les combinateurs, nous utilisons des continuations et une méthode de prédiction des premiers caractères acceptés par une grammaire. Sur la grammaire d'OCaml, on obtient en moyenne une analyse cinq fois plus lente qu'avec le parseur d'origine et deux fois plus rapide qu'avec Camlp4. De plus, on dispose de combinateurs inspirés de la notion de continuation délimitée pour optimiser les grammaires. Notons que nous gérons aussi les grammaires ambigües. Partie II (Christophe Raffalli) : Parser combinators are popular among functional programmers because they can be used to define languages parameterised by other languages and benefit from the strong type systems of the host language. Parser combinators have the reputation of being slow... However, with a few improvement, they become no more than five to ten times slower than stack automaton. It is easy to translate a BNF-like syntax into calls to combinators while keeping there advantages. However one main drawback remains: left recursion is forbidden. Although left recursion can easily be eliminated from a context free grammar, the presence of parametrised grammars requires more: a fixpoint combinator compatible with left recursion.

Thursday 26th February 2015 at 10h Andrea Frosini (Università degli Studi di Firenze),
Pattern avoiding polyominoes

Abstract: (Hide abstracts)
The concept of pattern within a combinatorial structure is an essential notion in combinatorics, whose study has had many developments in various branches of discrete mathematics. Among them, the research on permutation patterns and pattern-avoiding permutations has become very active. Nowadays, these researches have being developed in several other directions, one of them concerning the definition and the study of an analogue concept in other combinatorial objects. Some recent studies are presented here, concerning patterns in bidimensional structure, and, specifically, inside polyominoes. After introducing polyomino classes, I present an original way of characterizing them by avoidance constraints (namely, with excluded submatrices) and I discuss how canonical such a description by submatrix-avoidance can be. I also provide some examples of polyomino classes defined by submatrix-avoidance, and I conclude with some hints for future research on the topic.

Thursday 5th February 2015 at 10h30 TBA (TBA),
Séminaire Chocola

Thursday 29th January 2015 at 14h Jean-Louis Verger-Gaugry (LAMA),
Problème de Lehmer et fonctions zeta dynamiques limites

Abstract: (Hide abstracts)
En 1933 Lehmer enonce le problème suivant : existe-t-il une constante c > 0 telle que la mesure de Mahler M(α) de tout nombre algébrique α non nul et différent d’une racine de l’unité vérifie M(α) ≥ 1 + c. La Conjecture de Lehmer affirme que oui (C. Smyth, ”Survey”, 2014). Pour la tester de nombreuses familles de nombres algébriques tendant vers 1 ont été considérées. Il s'agit d’un problème limite et de minoration de M (ou de la hauteur pour des courbes elliptiques ou des variétés Abéliennes). Un autre problème limite ouvert est de caractériser le premier dérivé de l'ensemble des nombres de Salem T. Une première conjecture de Boyd dit que la réunion S ∪ T des ensembles des nombres de Pisot et de Salem est fermé. Une deuxième conjecture de Boyd affirme que le premier dérivé de l'ensemble des nombres de Salem est l'ensemble des nombres de Pisot. A chaque nombre algébrique réel β > 1 on peut souvent associer trois fonctions zeta dynamiques : (i) la fonction zeta d’Artin-Mazur de la beta-transformation ζ_β(z), qui provient du système dynamique de numération de Rényi-Parry, la base ́étant β; (ii) pour un polynôme P de petit hauteur s’annulant sur β, la fonction zeta de Lefshetz ζ_{L,β,P}(z), qui provient d’un automorphisme du tore n-dimensionnel, où n = deg P, et (iii) la fonction zeta d’Artin-Mazur ζ{AM,β,P}(z), qui provient de la même action sur le tore n-dimensionnel. Si (β_i) est une suite convergente de nombres algebriques, une question fondamentale est de savoir si les fonctions zeta limites peuvent apporter des solutions ou un éclairage nouveau sur ces questions ; par exemple, caractériser la limite des ensembles de pôles des fonctions ζ_{β_i}(z) lorsque i tend vers l'infini. En effet, le contrôle de la hauteur peut donner lieu à des phénomènes d'équidistribution limite de conjugués sur le cercle unité (Bilu, Petsche, Pritsker). On prendra l'exemple d'une famille F de nombres de Perron, qui tendent vers 1, racines dominantes de trinômes de hauteur 1 non réciproques, et de petite mesure de Mahler. On montrera que les développements asymptotiques (de Poincaré) des pôles des fonctions ζ_{β_i}(z) permettent d'obtenir le développement asymptotique de la mesure de Mahler et de prouver directement que la conjecture de Lehmer est vraie pour la famille F.

Thursday 22nd January 2015 at 10h Pierre Hyvernat (LAMA),
Représentation des fonctions continues entre ``streams'' (& Co.) par des types de données

Abstract: (Hide abstracts)
(Travail avec Peter Hancock) Brouwer savait déjà que les fonctions continues entre stream (avec la topologie produit habituelle) pouvaient être représentées par des arbres infinis. Peter Hancock a montré comment transformer ce ``théorème de représentation'' en théorie des types dépendant permettant de manipuler ces fonctions comme un type de données standard. Nous avons récemment pu généraliser ces idées à de nombreux types de données coinductifs en utilisant la notion de ``structure d'interaction'' (ou ``container indexé'' ou ``foncteur polynomial''). J'essaierais d'introduire les notions nécessaire au fur et à mesure : types dépendants, définitions inductives et coinductives, définitions inductive-récursives, etc.

Thursday 15th January 2015 at 10h Xavier Urbain (ENSIIE/CNAM),
Un cadre pour la preuve formelle adapté aux réseaux de robots mobiles

Abstract: (Hide abstracts)
Les réseaux de robots mobiles reçoivent depuis quelques années une attention croissante de la part de la communauté de l'algorithmique distribuée. Si l'utilisation d'essaims de robots coopérant dans l'exécution de diverses tâches est une perspective séduisante, l'analyse de la faisabilité de certaines tâches dans ce cadre émergent est extrêmement ardue, en particulier si certains robots présentent des comportements dits byzantins, c'est-à-dire arbitraires voire hostiles.

Pour obtentir des garanties formelles dans ce contexte, nous proposons un cadre mécanique formel fondé sur l'assistant à la preuve Coq et adapté aux réseaux de robots. Nous nous intéressons en particulier aux résultats d'impossibilité, fondamentaux en algorithmique distribuée en ce sens qu'ils établissent ce qui peut ou ne peut pas être réalisé et permettent de définir des bornes et, par là, l'optimalité de certaines solutions. Utiliser un assistant comme Coq travaillant à l'ordre supérieur nous permet d'exprimer aisément des quantifications sur les algorithmes, ceux-ci étant considérés comme des objets abstraits. Nous illustrons les possibilités offertes par notre développement en présentant les premières preuves formelles (et donc certifications) de certains résultats comme l'impossibilité de la convergence de robots amnésiques lorsqu'un tiers d'entre eux sont byzantins, ou encore l'impossibilité du rassemblement pour un nombre pair de robots évoluant dans R.

Thursday 4th December 2014 at 10h30 TBA (TBA),
Séminaire Chocola

Thursday 20th November 2014 at 10h Louis Cuel (LAMA),
Voronoi-based Geometric Inference

Abstract: (Hide abstracts)
Ces travaux s'inscrivent dans la thématique de l'inférence géométrique dont le but est de répondre au problème suivant : étant donné un objet géométrique dont on ne connaît qu'une approximation, peut-on estimer de manière robuste ses propriétés? On se place dans le cas où l'approximation est un nuage de points ou un ensemble digital dans un espace euclidien de dimension finie. On montre un résultat de convergence multigrille d'un estimateur du Voronoi Covariance Measure qui utilise des matrices de covariance de cellules de Voronoi. Ce résultat, comme la plupart des résultats en inférence géométrique, utilisent la stabilité de la fonction distance à un compact. Cependant, la présence d'un seul point aberrant suffit pour que les hypothèses des résultats de stabilité ne soient pas satisfaites. La distance à une mesure est une fonction distance généralisée introduite récemment qui est robuste aux points aberrants. Dans ce travail, on généralise le Voronoi Covariance Measure à des fonctions distances généralisées et on montre que cet estimateur appliqué à la distance à une mesure est robuste aux points aberrants. On en déduit en particulier un estimateur de normale très robuste. On présente également des résultats expérimentaux qui montrent une forte robustesse des estimations de normales, courbures, directions de courbure et arêtes vives. Ces résultats sont comparés favorablement à l'état de l'art.

Thursday 13th November 2014 at 10h30 TBA (TBA),
Séminaire Chocola

Thursday 23rd October 2014 at 10h Jacques-Olivier Lachaud (LAMA),
Multigrid-convergence of digital curvature estimators

Abstract: (Hide abstracts)
Many methods have been proposed to estimate differential geometric quantities like curvature on discrete data. A common characteristics is that they require (at least) one user-given scale parameter, that smooths data to take care of both the sampling rate and possible perturbations. Digital shapes are specific discrete approximation of Euclidean shapes, which come from their digitization at a given grid step. They are thus subsets of the digital plane Z^d. A digital geometric estimator is called multigrid convergent whenever the estimated quantity tends towards the expected geometric quantity as the grid step gets finer and finer. The problem is then: can we define curvature estimators that are multigrid convergent without such user-given parameter ? If so, what speed of convergence can we achieve ? We present here three digital curvature estimators that aim at this objective: a first one based on maximal digital circular arc, a second one using a global optimisation procedure, a third one that is a digital counterpart to integral invariants and that works on 2D and 3D shapes.

Thursday 16th October 2014 at 10h30 Breuvart Jacobé de Naurois Schmitz (Paris 7, Paris 13, Cachan),
Séminaire Chocola

Thursday 9th October 2014 at 10h Thomas Seiller (Institut des Hautes Études Scientifiques),
Des invariants de cohomologie pour la complexité?

Abstract: (Hide abstracts)
Je parlerai d'un travail récent qui se trouve à l'intersection entre la logique et la complexité algorithmique. Depuis plusieurs années, de nombreux systèmes logiques capturant des classes de complexité ont été étudiés, certains obtenus comme des systèmes dérivés de la logique linéaire de Girard -- les logiques linéaires bornées. En étudiant des modèles mathématiques de logiques linéaires bornées, on peut montrer une correspondance entre une hiérarchie de classes de complexité et une hiérarchie d'objets mathématiques -- les graphages. Ce résultat ouvre la porte à l'utilisation d'invariants de cohomologie définis sur les graphages en complexité.

Thursday 2nd October 2014 at 10h Clovis Eberhart (ENS Cachan),
Semrings, Partial Rings, and Weighted Language Equivalence

Abstract: (Hide abstracts)
Weighted automata are a structure that has many applications in computer science (speech recognition, natural language processing, image processing, quantitative modelling, etc). Weighted language equivalence is one possible semantics for these weighted automata. This equivalence is decidable for automata with weights on a field, but the proof relies heavily on the properties of fields. However, weighted automata can be defined more generally on a semiring, or even on structures where the addition is defined only partially. This talk explains how the result of decidability for weighted language equivalence for automata on fields can be extended to a decidability result for a certain class of semirings and ``partial semirings''.

Thursday 25th September 2014 at 10h30 Dal Lago. Schöpp. Vignudelli (Bologne, Munich, Bologne),
Séminaire Chocola

Thursday 4th September 2014 at 10h Flavien Breuvart (PPS),
De la caractérisation des modèles de H*

Abstract: (Hide abstracts)
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. Ce résultat sera notamment utilisé comme prétexte et exemple pour l'introduction d'un outil central dans ma thèse: les lambda-calculs avec tests. Il s'agit d'enrichir le lambda-calcul non typé avec des opérateurs directement issus du modèle dénotationnel impliqué afin de rendre celui-ci pleinement adéquat pour notre nouvelle syntaxe. Intuitivement, ces opérateurs vont internaliser un processus d'inférence de type possiblement divergent qui tente de typer l'arbre de Böhm d'un terme.``

Thursday 26th June 2014 at 10h Sébastien Labbé (LIAFA),
A d-dimensional extension of Christoffel words

Abstract: (Hide abstracts)
We extend the definition of Christoffel words to directed subgraphs of the hypercubic lattice in arbitrary dimension that we call Christoffel graphs. Christoffel graphs when d=2 correspond to well-known Christoffel words. Due to periodicity, the d-dimensional Christoffel graph can be embedded in a (d−1)-torus (a parallelogram when d=3). We show that Christoffel graphs have similar properties to those of Christoffel words: symmetry of their central part and conjugation with their reversal. Our main result extends Pirillo's theorem (characterization of Christoffel words which asserts that a word amb is a Christoffel word if and only if it is conjugate to bma) in arbitrary dimension. In the generalization, the map amb↦bma is seen as a flip operation on graphs embedded in ℤd and the conjugation is a translation. We show that a fully periodic subgraph of the hypercubic lattice is a translate of its flip if and only if it is a Christoffel graph.

Thursday 19th June 2014 at 10h Clément Aubert (Luminy),
Programmation logique, unification et espace logarithmique

Abstract: (Hide abstracts)
Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique. (En collaboration avec Marc Bagnol [ bagnol/], Paolo Pistone et Thomas Seiller [ seiller/])

Thursday 22nd May 2014 at 10h Karim Nour (LAMA),
Autour de la propriété de l'image(d'un terme) pour la théorie H

Abstract: (Hide abstracts)
La ``range property'' a été conjecturée par Böhm en 1968 et a résisté 16 ans avant d'être prouvée pour quelques théories du $lambda$-calcul. En 2007, A. Polonsky a montré que la conjecture est fausse pour la théorie $H$. Je présenterai dans cet exposé des conditions nécessaires pour que cette propriété soit vraie pour la théorie $H$. Je donnerai ensuite quelques pistes pour des extensions de ces résultats à d'autres systèmes.

Thursday 15th May 2014 at 10h Fabio Zanasi (ENS Lyon),
How to kill epsilons with a dagger - a coalgebraic take on systems with algebraic label structure

Abstract: (Hide abstracts)
We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $epsilon$-transitions. Our approach employs monads with a parametrized fixpoint operator $dagger$ to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems. This is joint work with Filippo Bonchi, Stefan Milius and Alexandra Silva.

Tuesday 15th April 2014 at 14h Keiko Nakata (Tallinn University of Technology),
Walking through infinite trees with mixed induction and coinduction: A Proof Pearl with the Fan Theorem and Bar Induction.

Abstract: (Hide abstracts)
We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of ``eventually always blueness '' and mixed inductive-coinductive ``almost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction).

Joint work with Marc Bezem and Tarmo Uustalu.

Thursday 3rd April 2014 at 13h30 Julien Leroy (Université du Luxembourg),
Caractérisation S-adique des sous-shifts minimaux de complexité inférieur à 2n+1

Abstract: (Hide abstracts)
Généralisant les systèmes dynamiques symboliques substitutifs, un système est dit $S$-adique si son langage est obtenue par itérations successives de substitutions appartenant à l'ensemble fini $S$. La suite de substitutions itérées en est alors une représentation $S$-adique et fournit des informations sur le système (minimalité, nombre de mesures ergodiques, fréquence des lettres,...). Dans cet exposé, je développerai une méthode basée sur les graphes de Rauzy et les mots de retour permettant de construire une représentation $S$-adique ``canonique''. Dans le cas des sous-shifts minimaux dont la différence première de complexité en facteur est majorée par 2 (contenant notamment les sous-shifts sturmiens, d'Arnoux-Rauzy ainsi que les codages de rotations et d'échange de 3 intervales), cette méthode fournit une caractérisation $S$-adique, où $S$ contient 5 substitutions. En particulier, cette caractérisation répond à la conjecture $S$-adique pour ce cas particulier.

Thursday 20th March 2014 at 10h Isar Stubbe (Université du Littoral-Côte d'Opale),
Eléments locaux, métriques partiels, diagonaux, et changement de base

Abstract: (Hide abstracts)
Quelle structure algébrique généralise à la fois les ensembles ordonnés et les espaces métriques? La structure de catégorie enrichie dans une catégorie monoïdale $mathcal{V}$, comme l'a montré Lawvere [1973]. En effet, si on pose $(mathcal{V},otimes,I)=([0,infty]^{sf op},+,0)$, alors la théorie des $mathcal{V}$-catégories est celle des espaces métriques; et si on pose $(mathcal{V},otimes,I)=({0,1},wedge,1)$, alors la théorie des $mathcal{V}$-catégories est celle des ensembles ordonnés. Mais comment faire si on veut parler des {em ensembles ordonnés d'éléments locaux}, autrement dit, des ensembles ordonnés ``dont les éléments ne sont pas définis partout''? Ou, dans le même esprit, si on veut parler des {em espaces métriques partiels}, c'est à dire, des espaces métriques ``dans lesquels la distance d'un point à lui-même n'est pas nécessairement zéro''? Je vais expliquer que, dans ces cas aussi, la structure recherchée est celle de catégorie enrichie---mais, cette fois, enrichie dans une bicatégorie $mathcal{W}$. De plus, pour les éléments locaux comme pour les métriques partiels, la bicatégorie $mathcal{W}$ en question est obtenue par une construction universelle sur une catégorie monoïdale $mathcal{V}$: c'est la {em la construction des diagonaux}. Donc, pour $(mathcal{V},otimes,I)=([0,infty]^{sf op},+,0)$, les $mathcal{V}$-catégories sont les espaces métriques; et pour $mathcal{W}=mathcal{D}(mathcal{V})$ (la bicatégorie des diagonaux dans $mathcal{V}$), les $mathcal{W}$-catégories sont les espaces métriques partiels. Mais bien sûr tout espace metrique ordinaire est un espace métrique partiel; et il est aussi vrai que tout espace métrique partiel détermine (au moins) un espace métrique ordinaire. Cette relation est entièrement expliquée par des {em changements de base}, c'est à dire des foncteurs particuliers, qui existent entre $mathcal{V}$ et $mathcal{W}$. Comme autre exemple de changement de base, je vais parler de l'ordre sous-jacent d'un espace métrique, et de l'espace métrique libre sur un ordre. Je vais par ailleurs indiquer comment, par le biais des changements de base, on peut formuler des questions pertinentes à propos de ces structures. Dans mon exposé, je vais éviter toute technicité (le seul prérequis étant la notion d'ensemble ordonné), car je veux surtout insister sur l'usage de bicatégories comme base d'enrichissement pour traiter spécifiquement les phénomènes décrits ci-dessus.

Thursday 27th February 2014 at 10h Michele Basaldella (Université d'Aix-Marseille),
Infinitary classical logic: recursive equations and interactive semantics

Abstract: (Hide abstracts)
In this talk, we present an interactive semantics for derivations (i.e., formal proofs) in an infinitary extension of classical logic. The formulas of our language are possibly infinitary (i.e., not necessarily well-founded, and not necessarily finitely branching) trees labeled by logical connectives and propositional variables. We show that in our setting every recursive formula equation has a unique solution. As for derivations, we use an infinitary variant of the standard Tait-calculus to derive sequents. In our sequent calculus, derivations are defined to be possibly infinitary trees labeled by sequents and rules. The interactive semantics we introduce is somehow similar to Girard's ludics, inasmuch as it builds upon a suitable procedure of cut-elimination. We show a completeness theorem for derivations, that we call interactive completeness theorem.

Thursday 20th February 2014 at 10h Luigi Santocanale (Laboratoire d'Informatique Fondamentale, Aix-Marseille Université),
Catégories mu-bicomplètes, jeux de parité, et élimination des coupures pour les preuves circulaires

Abstract: (Hide abstracts)
Dans cet exposé je présenterai la notion de catégorie mu-bicomplète, et instancierai cette notion avec la catégorie des ensembles, via la notion de jeu de parité. J'expliquerai ensuite l'importance de chercher un syntaxe adéquate pour dénoter toutes les flèches d'une catégorie mu-bicomplète libre. Je proposerai donc la notion de preuve circulaire (avec la condition sur les cycles qu'elle doit satisfaire) comme une telle syntaxe ; je justifierai cette proposition par les résultats de correction et complétude (fortes, catégoriels) du calcul, par rapport à la sémantique catégorielle envisagée. Nous montrerons qu'un théorème d’élimination des coupures vaut, car on peut éliminer les coupures d'un preuve circulaire finie avec cut, pour obtenir un arbre de preuve infini sans cut. Nous montrerons comment ce processus d’élimination des coupures amène à caractériser toutes les fonctions d'ensembles qui sont l'image d'une flèche d'une catégorie mu-bicomplete libre.

Thursday 6th February 2014 at 10h Laurent Vuillon (LAMA),
De la géométrie discrète à la biologie des interactions protéine-protéine

Abstract: (Hide abstracts)
Nous montrerons dans ce séminaire comment des outils mathématiques de géométrie discrète et de théorie des pavages peuvent servir à résoudre des problèmes de bio-mathématiques et en particulier de comprendre les interactions protéines-protéines. On va ainsi montrer comment ces interactions mènent à des polymères ``normaux'', à des virus ou à des fibres...

Thursday 19th December 2013 at 10h Olivier Bodini (Laboratoire d'Informatique de Paris-Nord),
Eléments de combinatoires analytiques pour l'analyse asymptotique et la génération aléatoire uniforme de convexes discrétisés

Abstract: (Hide abstracts)
Nous introduirons dans cet exposé quelques concepts de combinatoires analytiques (méthode symbolique, Théorèmes de transfert, Transformations de Mellin) et tenterons de montrer en quoi cette approche peut être utile pour certains problèmes de géométrie discrète. Plus particulièrement, nous nous intéresserons à l'étude asymptotique du nombre de convexes discrétisés de périmètre n. Cet exposé repose sur l'article ``Asymptotic Analysis and Random Sampling of Digitally Convex Polyominoes'', travail en commun avec P. Duchon, A. Jacquot et L. Mutafchief.

Thursday 5th December 2013 at 10h20 Johannes Kellendonk (Institut Camille Jordan),
A characterization of subshifts with bounded powers

Abstract: (Hide abstracts)
We say that a subshift, i.e. a closed shift invariant subspace of the space of sequences on a finite alphabet, has bounded powers. If there is an upper bound on the powers n with which words occur in the subshift. This is a strong combinatorial property which, for Sturmian susbshifts, coincides with the fact that the slope has bounded continued fraction expansion. Approximating the subshift space by a family of graphs we obtain a family of metrics which may or may not be Lipschitz equivalent. That latter property turns out to charactise minimal subshifts which have bounded powers.

Thursday 28th November 2013 at 10h Pierre-Étienne Meunier (Caltech),
Complexité de pavages auto-assemblants

Abstract: (Hide abstracts)
Les pavages auto-assemblants sont un modèle d'assemblage de structures moléculaires, implémentables avec de l'ADN, et capables de calcul Turing. J'expliquerai dans cet exposé deux bornes inférieures de complexité, dans le cas des systèmes d'assemblage non-coopératif (aussi appelés ``température 1'') : une sur les capacités de simulation intrinsèque du modèle, et l'autre sur la complexité d'assemblage de carrés de taille arbitraire.

Thursday 21st November 2013 at 10h Sébastien Labbé (LIAFA),
Construction de droites discrètes 3D par des suites S-adiques

Abstract: (Hide abstracts)
Les droites discrètes en 2D sont bien connues et possèdent plusieurs définitions équivalentes (combinatoire, arithmétique, dynamique). Toutefois, en dimension supérieure, ces définitions ne sont pas équivalentes et donnent lieu à des concepts différents : les mots de billards, les codages de rotations, les échange d'intervalles, le modèle standard de la droite discrète d'Éric Andres. Aucune de ces définitions de droites discrètes 3D ne conserve toutes les bonnes propriétés des droites discrètes 2D (suite équilibrée, complexité en facteurs linéaire). L'approche que nous considérons est la construction de droites discrètes par un produit de substitutions appelé suite S-adique selon la terminologie de Vershik et Livshits (1992). La suite de substitutions est déterminée par un algorithme de fractions continues multidimensionnelles donnant une suite d'approximations diophantiennes d'un vecteur de nombres réels. De récents résultats montrent qu'on peut construire des suites équilibrées (Delecroix, Hejda, Steiner, 2013) et de complexité linéaire en facteurs (Berthé, Labbé, 2013) avec cette approche.

Thursday 14th November 2013 at 10h Michaël Rao (ENS Lyon),
Quelques petits résultats et encore beaucoup de conjectures sur la suite de Kolakoski/Oldenburger

Abstract: (Hide abstracts)
La suite de Kolakoski, introduite - comme son nom ne le dit pas - par R. Oldenburger en 1939, est une suite auto-descriptive simple. Il s'agit de la suite 'w' sur l'alphabet {1,2} qui est égale à son propre ``run-length-encoding'' RLE(w). La ième lettre de RLE(w) est la taille du ième bloc de 'w', un bloc étant une répétition d'une même lettre. Cette suite commence donc par 12211212212211... Malgré sa définition simple, beaucoup de conjectures concernant cette suite sont ouvertes depuis une trentaine d'années. Il y a notamment la conjecture que la densité de 1 dans 'w' est 0.5. Concernant cette conjecture, la meilleure borne supérieure de 0.50084 a été donnée par V. Chvátal en 1993. Dans cet exposé, on verra cette suite comme un point fixe d'un transducteur. En prenant les puissances de ce transducteur, on obtiendra une nouvelle borne sur la densité. Cela nous permet également d'avoir un algorithme qui a permis d'explorer les 10^19 premières lettres de la suite. On finira par quelques nouvelles conjectures et questions sur cette suite.

Thursday 7th November 2013 at 10h Emmanuel Beffara (Institut de Mathématiques de Luminy),
Proofs as schedules

Abstract: (Hide abstracts)
This paper proposes a new interpretation of the logical contents of programs in the context of concurrent interaction, wherein proofs correspond to valid executions of a processes. A type system based on linear logic is used, in which a given process has many different types, each typing corresponding to a particular way of interacting with its environment and cut elimination corresponds to executing the process in a given interaction scenario. A completeness result is established, stating that every lock-avoiding execution of a process in some environment corresponds to a particular typing. Besides traces, types contain precise information about the flow of control between a process and its environment, and proofs are interpreted as composable schedulings of processes. In this interpretation, logic appears as a way of making explicit the flow of causality between interacting processes. Joint work with Virgile Mogbil.

Thursday 31st October 2013 at 10h Clovis Eberhar (ENS Cachan),
Relation entre parsing et pretty-printing

Abstract: (Hide abstracts)
Le parsing et le pretty-printing sont des opérations omniprésentes en informatique : communications entre machines ou entre processus, interfaces homme-machine, etc. Il semble évident que les parser et pretty-printer sont liés par une relation de cohérence, mais elle n'a jamais été mise en évidence. En conséquence, pour faire une preuve formelle utilisant un parser et un pretty-printer (par exemple d'un protocole de communication), il faut deviner une relation vérifiée par cette paire avant la prouver, ce qui rend la preuve difficile. Dans cet exposé, on donnera une définition de la cohérence entre un parser et un pretty-printer et on esseaira de la motiver.

Wednesday 23rd October 2013 at 13h30 Florian Hatat (Université de Savoie),
Jeux graphiques et théorie de la démonstration

Abstract: (Hide abstracts)
Ce travail est une contribution à la sémantique de jeux des langages de programmation. Il présente plusieurs méthodes nouvelles pour construire une sémantique de jeux pour un lambda-calcul de continuations. Si les sémantiques de jeux ont été développées à grande échelle pour fournir des modèles de langages fonctionnels avec références, en appel par nom et par valeur, ou pour différents fragments de la logique linéaire, certains de ses aspects demeurent cependant très subtils. Cette thèse s'intéresse spécifiquement à la notion d'innocence et à la combinatoire mise en jeu dans la composition des stratégies innocentes, en donnant pour chacune une interprétation via des constructions catégoriques standards. Nous reformulons la notion d'innocence en terme de préfaisceaux booléens sur une catégorie de vues. Pour cela, nous enrichissons la notion de parties dans notre sémantique de jeux en ajoutant des morphismes entre parties qui vont au-delà du simple ordre préfixe habituel. À partir d'une stratégie, donnée par les vues qu'elle accepte, on calcule son comportement sur toutes les parties en prenant une extension de Kan à droite. La composition des stratégies innocentes s'appuie sur les notions catégoriques habituelles de systèmes de factorisation et de foncteurs polynomiaux. Notre sémantique permet de modéliser l'interaction entre deux stratégies comme une seule stratégie dont il faut parvenir à cacher les coups internes, grâce à une technique d'élimination des coupures : cette étape est accomplie avec une version affaiblie des systèmes de factorisation. La composition elle-même entre stratégies repose pour sa part sur l'utilisation de la théorie des foncteurs polynomiaux. Les propriétés essentielles, telles que l'associativité ou la correction de la sémantique, proviennent d'une méthode de preuve presque systématique donnée par cette théorie.

Thursday 19th September 2013 at 10h Christophe Raffalli (Université de Savoie),
Nullstellensatz and Positivestellensatz from cut-elimination

Abstract: (Hide abstracts)
We give here an effective proof of Hilbert's nullstellensatz and Krivine-Stengle's positivestellensatz using the cut elimination theorem for sequent calculus. The proof is very similar to the current techniques in constructive algebraic geometry by Henri Lombardi, but seems more modular. In the case of the positive stellensatz, we think we prove a more general result than the original one, thanks to a new notion of justification of positiveness: PBDD (polynomial binary decision digram). It allows both to recover Krivine-Stengle's justification, but also another one which seems to require lower degree. We apply the same techniques to the nullstellensatz for differentially closed field and show that the proof is almost unchanged. Remark: here we do not provide bound, but an effective algorithm (implemented in OCaml) to build the wanted algebraic equality. Nevertheless, we discuss how bound could probably be obtained. We also do not deal effectively with the axiom of algebraic/real closure. Those are eliminated using standard model theory.

Thursday 27th June 2013 at 10h Robin Cockett (Dept. Computer Science, University of Calgary, Canada),
Abstract computability: unifying complexity and computability

Abstract: (Hide abstracts)
A benefit of abstract computability – which is the main subject matter of this talk – is that it allows the explicit unification of complexity and computability. Understanding the broader geography of these subjects is important for a number of reasons: it brings new perspectives to an old subject and it allows new tools to be brought to bear on old problems.

Abstract computability defines what one is modelling but is very flexible both on the how and the where. Of particular significance in this talk is the issue of where one models computability -- this flexibility adds a new dimension to computability. The talk demonstrates how complexity can be viewed as computability in the ``timed sets''. Significantly, this mimics precisely what complexity theorists actually do. The abstract approach, however, has the advantage of removing conceptual clutter and clarifying the structure of what is happening.

Abstract computability is based round the notion of a Turing category: the talk will introduce this and the necessary related structures.

Robin Cockett, Joaquin Diaz-Boïls, Jonathan Gallagher, Pavel Hrubes ``Timed Sets, Functional Complexity, and Computability'' Electronic Notes in Theoretical Computer Science Volume 286, 24 September 2012, Pages 117–137.

Robin Cockett, Pieter Hofstra ``Introduction to Turing Categories'' Annals of Pure and Applied Logic, Volume 156, Issues 2–3, December 2008, Pages 183–209

Tuesday 18th June 2013 at 10h Rodolphe Lepigre (LAMA, LIMD),
A Classical Realizability Interpretation of Judgement Testing

Abstract: (Hide abstracts)
A notion of test for intuitionistic type theory has been recently introduced by Peter Dybjer. It is meant to be the foundation for automatic testing tools that could be implemented in proof assistants such as Coq or Agda. Such tools would provide a way to test, at any time during the construction of a proof, if the current goal is typable in the context. The failure of such a test would mean that the goal is impossible to prove, and its success would corroborate the partial result. We investigate the possibility of extending the testing procedure to classical systems, and propose an interpretation of the testing procedure in term of Krivine's classical realizability.

Thursday 6th June 2013 at 10h Phuc NGO (Laboratoire d'Informatique Gaspard Monge),
Structure combinatoire des transformations rigides sur Z² : théorie et application à l'analyse topologique des images numériques

Abstract: (Hide abstracts)
Les transformations rigides (obtenues par composition de rotations et translations), lors qu’elles sont appliquées sur les imagesnumériques, sont généralement appliquées dans leur espace continu associé, nécessitant ensuite le recours à un procédé de digitalisation afin d’obtenir un résultat sur Z². Alternativement, nous proposons d'étudier ces transformations rigides dans un cadre totalement discret. En particulier, cette étude consiste à modéliser par une structure combinatoire (nommé, DRT graph) tout l'espace de paramètres de ces transformations sur les sous-ensembles de Z² de taille N × N. Ce graphe a une complexité spatiale de O (N^9). Nous décrivons cette structure combinatoire, et proposons également un algorithme permettant de la construire en temps linéaire par rapport à sa complexité spatiale. Le DRT graph peut être utilisé dans des applications de traitement d'images numériques, par exemple lors de procédures de recalage. Nous proposons ainsi des conditions pour lesquelles les images discrètes 2D préservent leurs propriétés topologiques pour toute transformation rigide. Nous en dérivons un procédé algorithmique permettant de vérifier l'invariance topologique des images par transformation rigide dans Z², où cette préservation n'est plus garantie contrairement à R². Cette étude est basée d'une part sur la notion de DRT graph, et d'autre part la notion de point simple. L'utilisation conjointe de ces deux notions permet notamment d'aboutir à une complexité en temps linéaire.

Thursday 30th May 2013 at 14h E. Domenjoud (LORIA (Equipe ADAGIo)),
Connexité par face des plans discrets et clôture palindromique géométrique

Abstract: (Hide abstracts)
Etant donné un vecteur non nul n de R^d et deux réels mu et w, le plan discret de vecteur normal n, de décalage mu et d'épaisseur omega, noté P(n,mu,omega), tel que défini par J.-P. réveillès, est l'ensemble des points de Z^d satisfaisant la double inégalité 0 <= <n,x> + mu < omega où <.,.> désigne le produit scalaire usuel dans R^d. Pour k dans {0,...d-1}, deux points distincts x et y de Z^d sont des k-voisins s'ils ont au moins k coordonnées communes et leurs coordonnées diffèrent d'au plus 1. Lorsque x et y sont représentés par des cubes unités centrés sur les coordonnées entières, ces cubes partagent alors une facette de dimension au moins k. Une partie S de Z^d est k-connexe, si pour toute paire de points x et y dans S, il existe dans S un chemin x=x_1,...,x_q=y formé de k-voisins. Le problème qui nous intéresse est, étant donnés un vecteur normal n et un décalage mu, de déterminer l'ensemble des valeurs de l'épaisseur omega pour lesquelles le plan P(n,mu,omega) est k-connexe. Nous nous intéressons plus particulièrement au cas où k=d-1, c'est à dire à la connexité par face. Cet ensemble est alors un intervalle infini à droite dont la borne inférieure est appelée épaisseur de connexité de n avec décalage mu et notée Omega(n,mu). Cette épaisseur peut être calculée grâce à un algorithme simple connu sous le nom d'algorithme totalement soustractif (Fully Subtractive Algorithm). Par définition, le plan P(n,mu,omega) est non connexe si omega < Omega(n,mu) et connexe si omega > Omega(n,mu). La question qui se pose alors est celle de la connexité de P(n,mu,Omega(n,mu)). Ce plan est presque toujours non connexe mais peut être connexe si la suite de vecteurs calculée par l'algorithme a une certaine propriété déterminée par Kraaikamp et Meester et qui n'est satisfaite que pour les vecteurs appartenant à un certain fractal de mesure nulle. La question de la connexité de P(n,mu,Omega(n,mu)) lorsque n appartient à ce fractal a été résolue dans un cas particulier en collaboration avec V. Berthé, D. Jamet et X. Provençal. Nous résolvons ici le cas général. Le déroulement de l'algorithme peut être décrit par un mot infini Delta sur l'alphabet {1,...,d}. A partir de ce mot, nous construisons une suite de sous-ensembles de Z^d qui, entre autres propriétés, sont connexes. Nous montrons que la limite de cette suite, appelée clôture palindromique géométrique itérée de Delta, est en fait P(n,0,Omega(n,0)) prouvant ainsi que ce plan est connexe. Nous exhibons également certaines valeurs particulières du décalage mu pour lesquelles P(n,mu,Omega(n,mu)) est non connexe. Le cas général lorsque mu est quelconque reste une question ouverte. (E. Domenjoud & L. Vuillon)

Thursday 30th May 2013 at 10h Ludovic Henrio (CNRS, INRIA Sophia-Antipolis),
Formal Models for Programming and Composing Correct Distributed Systems

Abstract: (Hide abstracts)
My research focuses on distributed programming models, more precisely using objects and components. In this area, I provided tools easing the programming of large-scale distributed applications and verifying their correct behaviour. To facilitate the programming of distributed applications, I contributed to the design and the development of languages with a high level of abstraction. My work aims to provide a strong model of programming languages, libraries, and runtime environments to the developer, and to guarantee the safe behaviour of distributed applications. In the OASIS team, we contributed to the definition of a distributed component model - the GCM (Grid Component Model) -, to its formalisation, and to its use for programming adaptive or autonomous components. After a short introduction to the principles of distributed computing and to the use of formal methods in this area, this talk will provide an overview of those aspects focusing on the programming models. I will conclude with a focus on a couple of my current research topics that include distributed algorithms for peer-to-peer systems, and programming on multicore and distributed architecture.

Thursday 23rd May 2013 at 10h30 Barbara Petit (Inria Grenoble),
LiDeAl: Certifying complexity with Linear Dependent Types

Abstract: (Hide abstracts)
Dependant Linear PCF (dlPCF) was introduced by Dal Lago and Gaboardi as a type system characterising the complexity of PCF programs. It is parametrised by a an equational program, which is used to express some complexity annotations for types. This enables a modular complexity analysis, and the main strength of the system is to be relatively complete: any terminating PCF program is typable in dlPCF (and its complexity is thus determined) assuming that the equational program is expressive enough. We have designed a type inference algorithm for this system: given a PCF program, it computes its type in dlPCF (and thus a complexity bound for the program) together with a set of proof obligations that ensures the correctness of the type, following the same scenario as the computation of weakest preconditions in Hoare logic. Checking formally the proof obligations generated by the type checker then amounts to a formal proof that the complexity bound is correct. In this talk I will explain how the type system dlPCF can be turned into a tool for formal certification of the complexity of functional programs.

Wednesday 17th April 2013 at 10h Emmanuel Beffara (IML),
À venir

Abstract: (Hide abstracts)
À venir

Thursday 4th April 2013 at 10h45 Fabio Zanasi (LIP, ENS Lyon),
Saturated Semantics for Coalgebraic Logic Programming

Abstract: (Hide abstracts)
A series of recent papers introduces a coalgebraic semantics for logic programming, where the behavior of a goal is represented by a parallel model of computation called coinductive tree. This semantics fails to be compositional, in the sense that the coalgebra formalizing such behavior does not commute with the substitutions that may apply to a goal. We suggest that this is an instance of a more general phenomenon, occurring in the setting of interactive systems (in particular, nominal process calculi), when one tries to model their semantics with coalgebrae on presheaves. In those cases, compositionality can be obtained through saturation. We apply the same approach to logic programming: the resulting semantics is compositional and enjoys an elegant formulation in terms of coalgebrae on presheaves and their right Kan extensions.

Thursday 28th March 2013 at 10h Tom Hirschowitz (LAMA, LIMD),
Un jeu pour le pi-calcul

Abstract: (Hide abstracts)
Dans un travail antérieur avec Damien Pous, on définit une sémantique pour CCS, qui peut être vue à la fois comme une sémantique de jeux non-déterministe et comme une sémantique de préfaisceaux innocents. Les résultats d'adéquation obtenus pour cette sémantique reposent sur le fait que les parties du jeu forment une catégorie fibrée, au sens de Grothendieck, au-dessus des positions. On s'attaque ici à poursuivre notre approche dans le cadre du pi-calcul. Or, s'il est facile de concevoir un jeu pour pi dans l'esprit de celui pour CCS, il est beaucoup moins évident que les parties sont fibrées au-dessus des positions. On montrera qu'elles le sont, en utilisant un outil catégorique bien connu: les systèmes de factorisation.

Thursday 21st March 2013 at 10h Pierre Hyvernat (LAMA, LIMD),
Test de terminaison pour PML : ``size-change termination'' et constructeurs (version propre)

Abstract: (Hide abstracts)
Il est en général indécidable de tester si une définition récursive est bien fondée, mais il existe de nombreux tests pour décider des conditions suffisantes pour la bonne fondation. Le principe du ``size-change'' de A. ben Amram, N.D. Jones et C.S. Lee est particulièrement simple (il s'agit simplement d'examiner certaines boucles dans le graphe d'appels des fonctions récursives), élégant (il repose sur le théorème de Ramsey) et puissant. C'est ce principe qui a été étendu et implanté dans le language PML. Les extensions vont dans deux directions : - autoriser la taille des arguments à augmenter localement, - utiliser la structure du langage (constructeurs / filtrage). Un point important est que ces extensions ne rendent pas le test plus compliqué à implanter.

Thursday 21st February 2013 at 10h Thomas Seiller (LAMA, LIMD),
Characterizing co-NL by a Group Action

Abstract: (Hide abstracts)
In a recent paper (Girard 2011b), Girard uses the geometry of interaction in the hyperfinite factor (Girard 2011a) in an innovative way to characterize complexity classes. The purpose of this paper is two-fold: to give a detailed explanation of both the choices and the motivations of Girard’s definitions, and – since Girard’s paper skips over some non-trivial details and only sketches one half of the proof – to provide a complete proof that co-NL can be characterized by an action of the group of finite permutations. We introduce as a technical tool the non-deterministic pointer machine, a concrete model that computes the algorithms represented in this setting.

Thursday 7th February 2013 at 14h Adrea Frosini (Università degli Studi di Firenze),
À venir

Abstract: (Hide abstracts)
À venir

Thursday 7th February 2013 at 10h Pablo Arrighi (LIG),
Generalized Cayley Graphs and Cellular Automata over them

Abstract: (Hide abstracts)
Cellular Automata can be characterized as the translation-invariant continuous functions, where continuity is with respect to a certain distance over the set of configurations. This distance, and its properties, easily extend from grids to Cayley graphs. As a consequence, Cellular Automata also extend from grids to Cayley graphs. Cayley graphs have a number of useful features: the ability to graphically represent finitely generated group elements and their equality; to name all vertices relative to a point; the fact that they have a well-defined notion of translation, and that they can be endowed with such a compact metric. But they are very regular. We propose a notion of graph associated to a language, which conserves or generalizes these features. These associated graphs can be arbitrary, although of a bounded degree. We extend Cellular Automata to these Generalized Cayley graphs, so that they define a local dynamics over time-varying graphs.

Thursday 31st January 2013 at 10h Étienne Miquey (LIP, ENS Lyon),
Réalisabilité et formules arithmétiques

Abstract: (Hide abstracts)
Dans le cadre de la réalisabilité classique telle qu'elle est introduite par Krivine, les réalisateurs |A| d'une formule A peuvent être vus comme des défenseurs de la formule face à une pile choisie parmi l'ensemble ||A|| de ses adversaires. Dans la continuité de cette interprétation, Krivine explique comment une formule arithmétique (∃xn, ∀yn, ... ∃x1, ∀y1 f(x, y)=0 ) peut être vue comme un jeu entre deux joueurs (∃ et ∀), un réalisateur étant alors une stratégie gagnante pour le jeu correspondant. Dans sa thèse, Guillermo montre que tout réalisateur universel est bien un stratégie gagnante. On montre ici que la réciproque est vraie : une stratégie gagnante est aussi un réalisateur universel. On s'intéresse ensuite à la relativisation des formules à différents types de données (et l'on montre qu'il existe dans le plus dur des jeux une stratégie gagnante valable pour toute formule vraie) et au lien entre formules d'atome f(x,y)=0 et f(x,y)<>0.

Thursday 24th January 2013 at 10h Guillaume Theyssier (LAMA, LIMD),
Automates cellulaires probabilistes

Abstract: (Hide abstracts)
Les automates cellulaires probabilistes ou non-déterministes sont souvent étudiés à travers des exemples ou aspects particuliers (alpha-asynchronisme, automates bruités, transitions locales probabilistes, etc). Nous proposons au contraire de les formaliser dans un modèle général qui se prête à une étude systématique. Partant de là nous abordons deux problématiques importantes largement développées dans la théorie des automates cellulaires déterministes : les simulations et l'universalité intrinsèque d'une part, la décidabilité des propriétés globales en fonction des descriptions locales d'autre part.

Thursday 20th December 2012 at 10h Clément Fumex (University of Strathclyde),
Schémas d'induction et de coinduction dans les fibrations

Abstract: (Hide abstracts)
En théorie des catégories, une fibration représente une forme d'indexation d'une catégorie par une autre. On rappellera comment une telle structure peut être utilisée pour modéliser une logique (représentée par la catégorie indexée) au dessus d'une théorie des types (représentée par la catégorie index). On portera alors notre attention sur les types inductifs et coinductifs et comment capturer leurs schémas d'induction et de coinduction respectif dans les fibrations.

Thursday 13th December 2012 at 10h Damien Pous (LIP, ENS Lyon),
Checking NFA equivalence with bisimulations up to congruence

Abstract: (Hide abstracts)
We introduce ``bisimulation up to congruence'' as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weaker ``bisimulation up to equivalence'' technique. The resulting algorithm can be exponentially faster than the recently introduced ``antichain algorithms''.

Thursday 29th November 2012 at 10h Marc Bagnol (IML),
Les machines synchrones: une catégorie à trace

Abstract: (Hide abstracts)
Les catégories à trace ont été utilisées dans le domaine de la sémantique dénotationnelle (en logique comme en informatique) pour modéliser des situations de rétroaction ``raisonnables''. La construction G(.) permet, à partir d'une catégorie à trace, d'obtenir une nouvelle catégorie dont la composition peut être vue comme une ``rétroaction parallèle''. Les ``machines synchrones'' ont été utilisées pour donner une sémantique des langages de programmation synchrones (Lustre, Esterel...) en termes d'automates. Dans ces sémantiques, la mise en parallèle de deux programmes est modélisée par une construction appelée ``produit synchrone''. On verra que les machines synchrones peuvent être vues comme une catégorie à trace S et que le produit synchrone de deux machines correspond à leur composition dans G(S).

Thursday 22nd November 2012 at 10h Jean-Marie Madiot (LIP, ENS Lyon),
Sous-typage en pi-calculs

Abstract: (Hide abstracts)
Le système de types input/output induit du sous-typage dans le pi-calcul. De manière un peu surprenante, le sous-typage se prête mal à une adaptation à des calculs proches (le calcul des fusions, le pi-calcul à mobilité interne). On construit une modification du calcul des fusions dans laquelle le mécanisme du sous-typage s'applique, ce qui permet d'en éclairer certains aspects.

Thursday 25th October 2012 at 10h Pierre Clairambault (Cambridge),
The biequivalence of locally cartesian closed categories and Martin-Löf type theories

Abstract: (Hide abstracts)
Seely’s paper Locally cartesian closed categories and type theory contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Löf type theories with Π, Σ, and extensional identity types. However, Seely’s proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely’s theorem: that the Bénabou-Hofmann interpretation of Martin-Löf type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-Löf type theories. As a second result we prove that if we remove Π-types the resulting categories with families are biequivalent to left exact categories.

Thursday 18th October 2012 at 10h Damiano Mazza (LIPN, Université Paris Nord),
Non-Linearity as the Metric Completion of Linearity

Abstract: (Hide abstracts)
It is well known that the real numbers arise from the metric completion of the rational numbers, with the metric induced by the usual absolute value. We seek a computational version of this phenomenon, with the idea that the role of the rationals should be played by the affine lambda-calculus, whose dynamics is finitary; the full lambda-calculus should then appear as a suitable metric completion of the affine lambda-calculus. We propose a technical realization of this idea: we introduce an affine lambda-calculus, based on a fragment of intuitionistic multiplicative linear logic; the calculus is endowed with a notion of distance making the set of terms an incomplete metric space; we show that the completion of this space yields an infinitary affine lambda-calculus, whose quotient under a suitable partial equivalence relation is exactly the full (non-affine) lambda-calculus. We also show how this construction brings interesting insights on some standard rewriting properties of the lambda-calculus (finite developments, confluence, standardization, head normalization and solvability).

Tuesday 9th October 2012 at 14h Romain Demangeon (Queen Mary, University of London),
Verification of Protocols with Session Types

Abstract: (Hide abstracts)
Introduced as symmetric types for pi-processes, session types have been developed into a large theory for verification of message-passing programs. Their main principle is as follows: a global type describing the expected interactions inside a network is projected into several local types: if every agent abides to its local type, the whole network abides to the global specification. I will present the Multiparty Session Types theory through recent developments: full-abstract embedding into the pi-calculus, nested protocols, automatic monitor generation, session types with multisession assertions.

Thursday 27th September 2012 at 10h Christophe Raffalli (LAMA, LIMD),
Réalisabilité, Ramsey et ultrafiltre

Abstract: (Hide abstracts)
On regardera les programmes que l'on peut extraire des preuves du théorème de Ramsey infini. On ira jusqu'à extraire un programme SML pour le ``happy ending problem'', qui trouve P sommets d'un polyogone convexe à partir de N points du plan si N est assez grand ( On regardera aussi le programme que donne la preuve de Ramsey par l'ultrafiltre par rapport à la preuve classique. Enfin, on se posera des questions sur les liens possibles entre la compléxité des programmes liés à Ramsey et des bornes sur la fonction de Ramsey.

Thursday 12th July 2012 at 14h30 Ivan Rapaport (CMM, Universidad de Chile),
Short messages and local knowledge in distributed systems

Abstract: (Hide abstracts)
We study distributed algorithms on massive graphs where links represent a particular relationship between nodes (for instance, nodes may represent phone numbers and links may indicate telephone calls). Since such graphs are massive they need to be processed in a distributed and streaming way. When computing graph-theoretic properties, nodes become natural units for distributed compu- tation. Links do not necessarily represent communication channels between the computing units and therefore do not restrict the communication flow. Our goal is to model and analyze the computational power of such distributed systems where one computing unit is assigned to each node.

Thursday 21st June 2012 at 11h Colin Riba (LIP, ENS Lyon),
A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Streams

Abstract: (Hide abstracts)
We discuss a complete axiomatization of Monadic Second-Order Logic (MSO) on infinite words (or streams). By using model-theoretic methods, we give an alternative proof of D. Siefkes’ result that a fragment with full comprehension and induction of second-order Peano’s arithmetic is complete w.r.t. the validity of MSO-formulas on streams. We rely on Feferman-Vaught Theorems and the Ehrenfeucht-Fraisse method for Henkin models of MSO. Our main technical contribution is an infinitary Feferman-Vaught Fusion of such models. We show it using Ramseyan factorizations similar to those for standard infinite words.

Thursday 14th June 2012 at 10h Anna Frid (Sobolev Institute of Mathematics),
Comptage des mots engendrés par intervalles

Abstract: (Hide abstracts)
Nous considérons la famille des problèmes reliés au comptage des mots sur un alphabet fini engendrés par intervalles, y compris les mots sturmiens, des mots de rotation et les mots engendrés par l'échange de trois intervalles. Nous discutons des méthodes géométriques et combinatoires de comptage.

Thursday 31st May 2012 at 10h Srecko Brlek (LaCIM, Université du Québec à Montréal),
Quelques remarques sur les trajectoires exponentielles d'Oldenburger

Abstract: (Hide abstracts)
Hedlund et Morse ont introduit et développé la dynamique symbolique vers 1938. La combinatoire des mots leur doit beaucoup, car ils ont mis en évidence de nombreux concepts important mais semblent avoir ignoré les trajectoires exponentielles de Rufus Oldenburger...

Thursday 24th May 2012 at 10h Pawel Sobocinski (University of Southampton, UK),
Combinators for Petri Nets with boundaries

Abstract: (Hide abstracts)
I will talk about two novel models of Petri nets with boundaries and characterise them using a calculus of combinators.

Wednesday 16th May 2012 at 10h15 Simon Perdrix (LIG, CAPP),
Completeness of algebraic CPS simulations

Abstract: (Hide abstracts)
The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the differential lambda calculus, the latter is a candidate lambda calculus for quantum computation. Their operational semantics differ in the treatment of applications and algebraic rules. We show how these two languages can simulate each other using an algebraic extension of the well-known call-by-value and call-by-name CPS translations. We prove that the simulations are sound and complete. Joint work with Ali Assaf, Alejandro Díaz-Caro, Christine Tasson and Benoît Valiron.

Thursday 3rd May 2012 at 10h Samer Allouch (LAMA, LIMD),
Classification des catégories finies

Abstract: (Hide abstracts)
On étudie dans cette thèse la relation entre les catégories finies et les matrices carrées positives, ensuite on arrive à étudier l'état de l'ensemble Cat(M) : s'il est vide ou non et déterminer ses bornes si c'est possible.

Thursday 26th April 2012 at 10h Tom Hirschowitz (LAMA, LIMD),
Une sémantique de jeux pour CCS (SUITE)

Abstract: (Hide abstracts)
(suite de l'exposé précédent) On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.

Sunday 1st April 2012 at 10h Karim Nour (LAMA, LIMD),
Les contres exemples d'Andrew Polonski

Abstract: (Hide abstracts)
(disponible prochainement)

Thursday 29th March 2012 at 10h Pascal Vanier (LIF, Marseille),
Degrés Turing des pavages

Abstract: (Hide abstracts)
Dans cet exposé, on étudie les ensembles de degrés Turing associés aux pavages générés par un jeu de tuile. En particulier, on prouve qu'il existe un quasi-isomorphisme entre n'importe quelle classe Pi01 de {0,1}^N et un pavage. Pour cela, on introduit une construction permettant d'avoir du calcul tout en ayant un nombre dénombrable de pavages.

Thursday 8th March 2012 at 10h Tom Hirschowitz (LAMA, LIMD),
Une sémantique de jeux pour CCS

Abstract: (Hide abstracts)
On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.

Thursday 19th January 2012 at 10h Etienne Duchesne (LIPN - Paris-Nord),
MELL in a free compact closure

Abstract: (Hide abstracts)
The categorical presentation of the standard model of the geometry of interaction –namely the free compact closure of sets and partial injections Int(PInj)– fails to be a denotational semantics of MELL. The work of Melliès, Tabareau & Tasson on the formula for a free exponential modality gives us insights into the reasons of this failure: absence of free pointed objects, absence of equalizers of some groups of permutations... We will present generic constructions which successively add the algebraic structure needed to compute this formula, and show that the usual model of GoI wrapped in these successive layers defines a denotational semantics of MELL.

Thursday 5th January 2012 at 10h Assia Mahboubi (LIX),
Vers une vérification formelle de la preuve du théorème de Feit-Thompson

Abstract: (Hide abstracts)
Le théorème de Feit-Thompson (1963) est un résultat historique de théorie des groupes finis. En effet, il permet de comprendre la structure de tous les groupes finis simples d'ordre impair et constitue ainsi une étape importante dans la classification des groupes finis simples qui est considérée comme achevée depuis les années 80. Néanmoins cette classification a un statut controversé car elle résulte de la compilation d'un nombre considérable de publications hétérogènes et parfois encore mal comprises. La preuve du théorème de Feit-Thompson est elle-même imposante, par sa taille et par la variété des résultats sur lesquels elle repose (théorie des groupes, algèbre linéaire, théorie de Galois, caractères,...). Elle est un défi pour les assistants à la preuves, logiciels permettant de représenter énoncés et preuves mathématiques sous la forme de termes logiques, vérifiables mécaniquement par un ordinateur. Dans cet exposé, qui ne présuppose aucune connaissance préalable en théorie des groupes, nous essaierons de montrer quels problèmes sont posés par une telle formalisation, par la représentation des objets mathématiques mis en jeu en théorie des types et en particuliers les solutions qui ont été trouvées pour faire vérifier (une partie conséquente de) cette preuve par l'assistant à la preuve Coq.

Thursday 15th December 2011 at 10h Annette Casagrande (LAMA, LIMD),
Proposition d'une mesure de voisinage entre textes Application à la veille stratégique

Abstract: (Hide abstracts)
Nous proposons une méthode de calcul de proximité entre textes, appelée mesure de voisinage. Cette mesure est basée sur la présence de mots communs, de synonymes et de mots cooccurrents. Nous comparons cette mesure à la similarité cosinus, utilisée en Recherche d'Informations, au travers de trois bases de données différentes. Nous avons développé un prototype, nommé ALHENA, utilisé dans le domaine de la veille stratégique anticipative (VAS). L'expérimentation menée sur la valorisation du CO2 a montré l'utilité du prototype dans le processus de VAS, face au problème de la surcharge d'information notamment occasionnée par l'usage de l'Internet.

Thursday 1st December 2011 at 10h Karim Nour (LAMA, LIMD),
About the range property for H

Abstract: (Hide abstracts)
Recently, A. Polonsky has shown that the range property fails for H. We give here some conditions on a term F that imply that its range has cardinality either 1 or infinity. L'exposé sera accessible à tous les membres de l'équipe.

Thursday 17th November 2011 at 10h Krzysztof Worytkiewicz (LAMA),
Simulations as homotopies

Abstract: (Hide abstracts)
We exhibit a model structure on 2-Cat. A certain class of homotopies in this model structure turns out to be in 1-to-1 correspondence with strong simulations among labeled transitions systems, formalising the geometric intuition of simulations as deformations. The correspondence still holds in the cubical setting, characterising simulations of higher-dimensional transition systems (HDTS).

Thursday 20th October 2011 at 10h Lionel Vaux (LDP, IML),
On the transport of finiteness structures

Abstract: (Hide abstracts)
Finiteness spaces were introduced by Ehrhard as a model of linear logic, which relied on a finitess property of the standard relational interpretation and allowed to reformulate Girard's quantitative semantics in a simple, linear algebraic setting. I will review recent results obtained in a joint work with Christine Tasson, providing a very simple and generic construction of finiteness spaces: basically, one can ``transport'' a finiteness structure along any relation mapping finite sets to finite sets. Moreover, this construction is functorial under mild hypotheses, satisfied by the interpretations of all the positive connectives of linear logic. Recalling that the definition of finiteness spaces follows a standard orthogonality technique, fitting in the categorical framework established by Hyland and Schalk, I will show that the features of transport do not stand on the same level as the orthogonality category construction; rather, they provide a simpler and more direct characterization of the obtained structure, in a webbed setting. PS: Although I have slides (in english) ready for this presentation, it is best enjoyed in its chalk and blackboard version so I will stick to the latter.

Thursday 6th October 2011 at 10h Tim Porter (WIMCS, University of Bangor),
Homotopical Aspects on Multiagent Systems

Abstract: (Hide abstracts)
The epistemic logic used for n-agent systems is the modal logic $S5_n$. In this talk I will briefly look at the Kripke semantics of this, how it relates to simple models of multiagent systems, and then will explore some ideas that make some tentative steps in the direction of modelling the flow information and knowledge in such systems. (The last part will raise more problems and questions than it answers but that is the fun of it!!! Since the paper below was written, directed homotopy has been developed more and it remains to be seen if it can be used to describe evolving multi-agent systems. I will discuss this beyond the prepared slides, if there is time.) (As I have slides in English, I will give the talk in that language.) Ref: Interpreted systems and Kripke models for multiagent systems from a categorical perspective, Theoretical Computer Science, 323 (2004) pp. 235-266.

Thursday 29th September 2011 at 10h Pawel Gladki (AGH University of Science and Technology, Kraków, Poland),
Quotients of index two of the space of orderings of the field Q(x)

Abstract: (Hide abstracts)
Let $(X,G)$ be a space of orderings, let $G_0$ be a subgroup of index $2$ in $G$, $-1 in G_0$, and let $X_0$ denote the set of restrictions $X restriction G_0$ of elements of $X$ (viewed as characters on $G$) to characters on $G_0$. We search for necessary and sufficient conditions on $G_0$ for $(X_0,G_0)$ to be a quotient of $(X,G)$. In particular, we discuss the case when $(X,G)$ is the space of orderings of the field $Q(x)$. The talk is intended for a broad audience and all definitions necessary to follow the exposition will be explained in details. This is joint work with Murray Marshall.

Thursday 22nd September 2011 at 10h Pierre Hyvernat (LIMD),
Foncteurs polynomiaux, jeux et logique linéaire (différentielle)

Abstract: (Hide abstracts)
Les « systèmes d'interaction » étaient à l'origine un moyen de représenter une notion de « jeux » en théorie des types. On obtient de cette manière une catégorie de jeux et de simulations qui modélise la logique linéaire différentielle. De manière assez surprenante, la dynamique ne joue aucun rôle dans la définition de composition des stratégies ! Cette notion de jeux existe sous des noms différents : « containers » (Ghani, Altenkirch, Hancock, ...) ou « foncteurs polynomiaux » (Hyland, Kock, Gambino, ...). Ce qui change ici est la notion de morphisme, plus générale que dans la littérature existante. Après une petite introduction, je montrerais les liens entre ces polynômes (point de vue intentionnel) et les foncteurs associés (point de vue extensionnel). Je construirais ensuite le modèle de (D)ILL en insistant sur l'interprétation en termes de jeux et les similarités formelles avec le modèle « dégénéré » des transformateurs de prédicats. Je ne ferais probablement aucune preuve, mais je mentionnerais quand même l'outil important, à savoir le langage interne des catégories localement cartésiennes fermées (càd la théorie des types dépendants)...

Thursday 7th July 2011 at 10h09 Pierre Hyvernat (LIMD),
Petit casse-tête combinatoire : sections non-ordonnées et fonctions booléennes strictement croissantes

Abstract: (Hide abstracts)
On muni les tuples d'ensembles d'entiers (X1, ..., Xn) de l'ordre suivant : (X1, ..., Xn) < (Y1, ..., Yn) si les Xs ont plus de « sections non-ordonnées » que les Ys. L'équivalence engendré par ce préordre est très simple, mais la preuve, bien qu'élémentaire, l'est moins (il s'agit d'un petit casse-tête amusant...). Je caractériserais cette équivalence (avec la preuve) ainsi que les liens entre cet ordre et l'inclusion toute simple. La preuve utilise la notion de fonction booléenne strictement croissante, qui semble ne pas apparaitre souvent dans la littérature. Je montrerais quelques unes de leurs propriétés. Pré-requis : notion d'ordre, de permutation, de quotient. (niveau L1)

Thursday 30th June 2011 at 11h Yukiko Kenmochi (Laboratoire d'Informatique Gaspard-Monge, Université Paris-Est),
L'ajustement robuste d'un hyperplan discret

Abstract: (Hide abstracts)
Nous considérons le problème d'ajustement suivant : étant donné un ensemble de N points dans une image numérique en dimension d (i.e. Z^d), trouver un hyperplan discret qui contient le plus grand nombre possible de points. En utilisant un modèle discret pour l'hyperplan, nous montrerons que nous pouvons générer tous les ensembles de consensus possibles pour ajuster le modèle, et présenterons une méthode exacte pour d=2,3 dont la complexité en temps est O(N^d log N) et celle en espace est O(N). Ces complexités ont naturellement motivé l'amélioration. Nous avons ensuite observé que le problème est 3SUM-difficile pour d=2 de sorte qu'il ne peut probablement pas être résolu exactement avec une complexité meilleure que O(N^2), et il est conjecturé que la complexité optimale en dimension d est en fait O(N^d). Nous proposons donc deux méthodes approximatives de complexité linéaire en temps.

Thursday 16th June 2011 at 14h30 Mohamad Ziadeh (LIMD),
Completness for simply typed lambda mu calculus

Abstract: (Hide abstracts)
Between the important thing, when we deal with a type or a formula A of a system of typing that satisfies the strong normalization S.N., is to build a set of terms that satisfies 'a term in the set corresponding to A is equivalent to say that t is of type A. Unfortunally it is impossible to have this equivalency because of S.N., so the work take another formulation to escape this problem and it becomes 'a term in the set corresponding to A is equivalent to say that t is in relation with t' which is of type A'. many studies having this form where been published for many systems and relations. My work will be around the simply typed system in lambda mu calculus.

Thursday 9th June 2011 at 10h Nicolas Michel (EPFL),

Abstract: (Hide abstracts)
La définition des différentes K-théories suit le schéma suivant. Etant donné un objet C, on lui associe d'abord une catégorie AC qui est « structurée » (symétrique monoïdale, exacte, Waldhausen, …). On applique ensuite une « machine » de K-théorie sur AC pour obtenir finalement le spectre de K-théorie de l'objet C. Par exemple, on associe à un anneau R sa catégorie de modules projectifs de type fini pour obtenir la K-théorie usuelle de R. Dans ma thèse, je me suis intéressé à la première étape de ce processus. Plus précisément, je me suis posé les questions suivantes. Quels types d'objets admettent une notion intéressante de K-théorie ? Quelles catégories structurées devrait-on associer à ces objets pour obtenir une information K-théorique à leur sujet ? Finalement, comment cette correspondance prend-elle en compte les morphismes de ces objets ? Je vais décrire un cadre conceptuel qui permet de traiter de manière unifiée de nombreux exemples et qui apporte de nouveaux outils pour les étudier. Je prendrai l’exemple de la K-théorie des schémas comme fil conducteur.

Thursday 26th May 2011 at 10h03 Christophe Raffalli (LIMD),
(Co-)Inductive type : subtyping may be enough

Abstract: (Hide abstracts)
We present here a strongly normalizable extension of second order functional arithmetics (AF2) with subtyping, that allows to program with recursive types in the pure lambda-calculus (i.e., without constant). It assigns types to the Scott encoding of algebraic datatypes and to the recursor on those types. Thus, it answers the open question of finding a strongly normalizing type system which allows to program on Scott numerals. One of the key features of the system is to have no more typing rules than AF2. The new rules are only subtyping rules. The first-order layer is used to prove the correction of extracted programs. It is also worth noticing that in this system union type (both finite and infinite) are definable and still the system enjoys subject-reduction.

Thursday 19th May 2011 at 10h05 Luidnel Maignan (INRIA Saclay),
Points, Distances and Cellular Automata: Geometric and Spatial Algorithmics

Abstract: (Hide abstracts)
Spatial computing aims at providing a scalable framework where computation is distributed on a uniform computing medium and communication happen locally between nearest neighbors. We study the particular framework of cellular automata, using a regular grid and synchronous update. As a first step towards generic computation, we propose to develop primitives allowing to structure the medium around a set of particles. We consider three problems of geometrical nature: moving the particles on the grid in order to uniformize the density, constructing their convex hull, constructing a connected proximity graph establishing connection between nearest particles. The last two problems are considered for multidimensional grid while uniformization is solved specifically for the one dimensional grid. The work approach is to consider the metric space underlying the cellular automata topology and construct generic mathematical object based solely on this metric. As a result, the algorithms derived from the properties of those objects, generalize over arbitrary regular grid. We implemented the usual ones, including hexagonal, 4 neighbors, and 8 neighbors square grid. All the solutions are based on the same basic component: the distance field, which associates to each site of the space its distance to the nearest particle. While the distance values are not bounded, it is shown that the difference between the values of neighboring sites is bounded, enabling encoding of the gradient into a finite state field. Our algorithms are expressed in terms of movements according to such gradient, and also detecting patterns in the gradient, and can thus be encoded in finite state of automata, using only a dozen of state.

Tuesday 17th May 2011 at 10h06 Vincenzo Ciancia (Amsterdam, ILLC),
Labelled transition systems with interfaces and symmetry: coalgebras in a presheaf category and their finite representations

Abstract: (Hide abstracts)
In this talk, we discuss how to model in a finite way the semantics of resource-allocating interactive programs. Surprisingly, in doing so, the notion of behavioural symmetry arises from the framework, and is necessary to recover canonical models. Behavioural symmetry expresses properties relating the semantics of a program and the available resources at each state, e.g. ``the distinguished variables x and y have the same observable effect, and swapping them does not affect the semantics of the program''. Labelled transition systems (LTSs) have been successfully used to model the semantics of interactive programming languages. Their natural equivalence relation, the so-called bisimilarity, is a fundamental tool for the study of such languages. However, when resources (e.g. memory locations) can be allocated and de-allocated along transitions, bisimilarity becomes a non-standard notion (cf. the pi-calculus). The categorical abstraction of coalgebras generalises LTSs and has an associated, general definition of behavioural equivalence, coinciding with bisimilarity for LTSs. Presheaves generalise classical sets; elements of presheaves have intensional features such as interfaces, or resources, and operations on them. By using coalgebras in a category of presheaves, bisimilarity in the presence of resource allocation is recovered from the standard categorical definition. However, the obtained transition systems become infinite state machines because of fresh resources. An equivalence between categories of presheaves and of families recovers a finite representation for memory-bound programs. An associated notion of symmetry is necessary for the equivalence to hold, and for final systems (=canonical models) to exist, giving rise to behavioural symmetry.

Thursday 12th May 2011 at 10h06 Tom Hirschowitz (LAMA (LIMD)),
Introduction aux faisceaux

Abstract: (Hide abstracts)
Cet exposé, faisant suite au précédent sur les préfaisceaux, est une introduction aux faisceaux, un autre important outil catégorique dérivé des premiers. Je rappellerai le lemme de Yoneda, puis définirai les notions de crible, topologie de Grothendieck et enfin faisceau, en m'appuyant sur des exemples et contre-exemples. Si le temps le permet, je survolerai le théorème du faisceau associé, qui construit un faisceau à partir d'un préfaisceau arbitraire (si Christophe est là, on parlera de PML). Enfin, peut-être, je raconterai en deux mots mon travail avec Damien Pous, qui repose sur une description en termes de faisceaux des stratégies dites ``innocentes'' en sémantique des jeux.

Thursday 21st April 2011 at 10h Lionel Nguyen Van Thé (LATP (Marseille)),
Théorie de Ramsey, points fixes d'actions de groupes et correspondance de Kechris-Pestov-Todorcevic

Abstract: (Hide abstracts)
En 1998, Pestov montra que le groupe G des automorphismes des rationnels (vus comme ensemble ordonné) est extrêmement moyennable, c'est-à-dire que toute action continue de G sur tout espace topologique compact admet un point fixe. Pour ce faire, il démontra que la propriété énoncé ci-dessus est équivalente au théorème de Ramsey fini. Ce résultat constitue le point de départ des travaux de Kechris, Pestov et Todorcevic, qui établirent en fait qu'il s'agit là d'un phénomène général liant théorie de Ramsey pour certaines classes de structures finies (classes de Fraïssé) et moyennabilité extrême pour certains groupes topologiques. Le but de cet exposé sera de présenter la correspondance de Kechris-Pestov-Todorcevic ainsi que certaines de ces conséquences.

Thursday 14th April 2011 at 10h Tom Hirschowitz (LAMA (LIMD)),
Introduction aux prefaisceaux

Abstract: (Hide abstracts)
Cet exposé est une introduction aux préfaisceaux, un important outil catégorique. Je reprendrai du début: catégories, foncteurs, transformations naturelles, en considérant de nombreux exemples petits et gros. Je concluerai par le lemme de Yoneda en donnant l'exemple des graphes.

Thursday 31st March 2011 at 10h14 Peter G. Hancock (University of Strathclyde),
Distillation of inductive-recursive definition

Abstract: (Hide abstracts)
`IR' is a powerful principle for in the context of dependent type-theory, for defining simultaneously a set U *inductively*, with a function T : U -> D *recursively*. D may be `large', eg the type of Sets, and a paradigm example is a universe of (codes for) sets. I will try to motivate and illustrate this principle. Using containers (a particular kind of endofunctor on Set), one can distill out the essence of IR in an extremely compact, memorable form. I will try to give a tour of the distillery.

Thursday 24th March 2011 at 10h11 Alina FIRICEL (Institut Camille Jordan),
Automates finis et séries de Laurent algébriques

Abstract: (Hide abstracts)
Dans cet exposé, nous montrerons comment utiliser la combinatoire des mots et la théorie des automates afin d'étudier certaines propriétés arithmétiques des séries de Laurent à coefficients dans un corps fini. En particulier, à l'aide d'une méthode inspirée par un article d'Adamczewski et Cassaigne, nous donnerons une majoration générale de l'exposant d'irrationalité des séries algébriques. Nous illustrerons cette approche à l'aide de quelques exemples.

Thursday 17th March 2011 at 10h11 Peter G. Hancock (University of Strathclyde),
Logarithms and exponentiality

Abstract: (Hide abstracts)
I shall dust off some work by Bohm, on arithmetical features of combinatory logic. The natural combinators for addition, multiplication, exponentiation and nihilation of Church satisfy some pleasing algebraic laws resembling those of ordinal arithmetic. But they also satisfy and some other ''wild'' laws (resembling nothing arithmetical) in virtue of which they are combinatorially complete. Because of that, they support a notion of logarithm (with respect to a ''base''). I may add some remarks on ''exponentiality'', which says that two ''numbers'' are the same if they have the same behaviour as exponents.

Thursday 10th February 2011 at 10h03 Vincent Nesme (University of Potsdam),
Automates cellulaires linéaires et fractales

Abstract: (Hide abstracts)
Tout le monde aime les automates cellulaires, tout le monde aime les fractales, et l'on sait bien que celles-ci peuvent être produits par ceux-là. Par exemple, le triangle de Sierpinski, comme il s'agit du triangle Pascal modulo 2, est le diagramme espace-temps limite d'un automate cellulaire correspondant à la relation C(n+1,k+1)=C(n,k)+C(n,k+1). Plus généralement, il est connu que si l'alphabet a une structure d'anneau commutatif et que l'automate cellulaire est un morphisme d'anneaux - on parle alors d'automate cellulaire linéaire - une structure fractale va émerger de ses diagrammes espace-temps. Remplaçons maintenant l'anneau par un simple groupe - non, pas un groupe simple, un simple groupe abélien fini. J'expliquerai pourquoi, à mon sens, c'est dans ce cas plus général qu'on devrait parler d'automate cellulaire linéaire, et non pas seulement dans le cas des anneaux comme on le fait habituellement ; et surtout, je tâcherai de faire comprendre pourquoi leurs diagrammes espace-temps ont aussi des propriétés fractales.

Thursday 20th January 2011 at 10h07 Pierre Hyvernat (LIMD),
Le principe du ``size-change termination'' pour les langages avec constructeurs

Abstract: (Hide abstracts)
Le ``size-change termination principle'' est un test (correct mais forcément incomplet) pour décider la terminaison de programmes mutuellement récursifs. Ce test, dû à A. ben Amram, N.D. Jones et C.S. Lee est particulièrement simple et élégant, tout en étant relativement puissant et modulaire. Il s'agit essentiellement d'une opération de clôture transitive sur le graphe d'appels des fonctions et la preuve de correction repose sur le théorème de Ramsey infini. Quand le langage des définitions récursives est un langage avec constructeurs / destructeurs à la ML, il y a une notion naturelle de taille : le nombre de constructeurs dans une valeur. Dans ce contexte, on peut généraliser le test pour conserver plus d'information que la seule taille des arguments. Ceci permet notamment d'ignorer certains chemins du graphe d'appels qui ne correspondent à aucune suite concrète d'appels. Par contre, la preuve de correction du nouveau principe est plus complexe que l'originale. Après une rapide présentation du test original, je décrirais cette extension et donnerai certaines idées de la preuve de correction. Comme le test est implanté (en Caml) pour le langage PML, je donnerais également des exemples (et ``contre exemples'') pour permettre de se faire une idée des définitions acceptées (et refusées).

Thursday 13th January 2011 at 10h03 Thomas Seiller (Institut mathématique de Luminy),
Graphes d'interaction

Abstract: (Hide abstracts)
Je présenterai un modèle localisé de la logique linéaire multiplicative basé sur des graphes à partir duquel il est possible d'obtenir une catégorie *-autonome ainsi que de définir une notion de vérité. Je montrerai également qu'une restriction de ce modèle à une certaine classe de graphes se plonge dans la géométrie de l'interaction hyperfinie de Girard. Ceci permet d'appréhender de manière purement combinatoire le cadre utilisant des éléments d'analyse fonctionnelle avancés introduit par Girard. J'expliquerai enfin comment adapter ce modèle pour l'étendre à la logique linéaire multiplicative-additive, et discuterai d'une extension aux exponentielles.

Friday 31st December 2010 at 10h10 Guillaume Theyssier (LAMA),
Trilogie autour de la ligne de fusiliers

Abstract: (Hide abstracts)

Thursday 25th November 2010 at 14h Mouhammad Said (LIMD),
Géométrie multi-résolution des objets discrets bruités.

Abstract: (Hide abstracts)
Les courbes frontières définissent les régions ou les formes du plan de manière compacte et descriptive. Il est bien connu que les formes doivent être étudiées à différentes échelles. Ceci a conduit au développement des pyramides régulières et irrégulières pour l'analyse des formes et la compréhension des scènes. Cependant, il n'existe pas une description analytique de la multi-résolution d'une forme numérique, contrairement au célèbre espace-échelle (scale-space) dans le monde continu. En outre, les primitives géométriques telles que les lignes, les cercles ou les polynômes ont une grande importance dans le contexte de la géométrie numérique. Les morceaux des droites numériques sont un bon moyen pour estimer les tangentes et les arcs discrets approchent la courbure. Il est donc nécessaire de les garder dans l'analyse multi-échelle des frontières numériques. Un des objectifs de cette thèse est de donner des nouveaux résultats analytiques sur la multi-résolution des droites 4-connexes et des segments de droites 4-connexes. Figueiredo est le premier qui a étudié le comportement des droites 8-connexes lors du changement de la résolution de la grille. Dans le présent travail, nous considérons une droite 4-connexe pour laquelle une description analytique est fournie lorsque la résolution de la grille est modifiée par un facteur arbitraire. En plus, nous montrons que leurs couvertures sont des droites 4-connexes. Comme les formules analytiques des segments de droite sont un problème beaucoup plus difficile, nous proposons un parcours indirect pour la multi-résolution d'un DSS en utilisant le fait qu'un segment est un morceau fini d'une droite discrète. Etant donné un DSS, nous construisons deux droites dont l'intersection le contient et dont la partie connexe principale a les mêmes caractéristiques arithmétiques, ainsi que le même nombre de motifs. Notons que nous proposons de nouveaux résultats combinatoires des intersections de droites. Nous déterminons la multi-résolution du segment en examinant la multi-résolution de l'intersection de ces deux droites. Nous donnons une nouvelle description analytique de cet ensemble avec les inégalités arithmétiques. Nous abordons également le problème du calcul des caractéristiques exactes d'un sous-segment d'une droite 4-connexe qui a des caractéristiques connues. Nous présentons deux nouveaux algorithmes SmartDSS et ReversedSmartDSS qui résolvent ce problème. Leur principe est de se déplacer dans l'arbre de Stern-Brocot de la fraction soit de manière haut-bas ou bas-haut. Dans le pire cas, leur complexité est meilleure que l'algorithme de reconnaissance DSS classique. Les deux algorithms peuvent dès lors servir à calculer efficacement la multi-résolution d'un segment. Les bruits tout au long des contours numériques ne sont pas vraiment détectés, mais plutôt annulés par l'épaississement des segments de droites 4-connexes. De plus, l'épaisseur est réglée par un utilisateur et aussi définie globalement pour le contour. Pour surmonter ce problème, nous proposons une stratégie originale pour détecter localement à la fois la quantité de bruit et les épaisseurs significatives de chaque point de contour. Ce travail se base sur les propriétés asymptotiques de segments flous d'épaisseurs différentes, et forme une alternative à l'approche multi-résolution de la détection du bruit.

Thursday 25th November 2010 at 10h03 Gabriele Fici (I3S, Université de Nice),
Une nouvelle approche à l'étude des mots C∞

Abstract: (Hide abstracts)
La classe des mots C∞, ou facteurs lisses, est la classe des mots finis qui sont arbitrairement dérivables. Ils ont été défini par Dekking pour décrire l'ensemble des facteurs du fameux mot de Kolakoski, le mot infini point fixe du codage par plages. Nombre de conjectures sur le mot de Kolakoski et ses facteurs restent ouvertes. Nous introduisons une nouvelle représentation des mots C∞ basée sur un codage de ces mots sur un alphabet à trois lettres. Ceci permet de classifier les mots C∞ en classes d'équivalence. Ces classes d'équivalence peuvent être représentées sur un graphe infini dont nous étudions les propriétés. Nous démontrons que ce graphe peut être décrit inductivement par une fonction récursive dont la définition est totalement indépendante du contexte des mots C∞.

Thursday 14th October 2010 at 10h09 Émilie Charrier (LAMA),
Vers un estimateur de bruit local sur les surfaces discrètes

Abstract: (Hide abstracts)
B. Kerautret et J.-O. Lachaud ont proposé en 2009 un estimateur de bruit local sur les contours discrets 2D. Leur méthode consiste en une analyse multi-échelle des longueurs des segments maximaux en chaque point du contour. L'étude de la courbe du profil multi-échelle et la connaissance du comportement asymptotique de ces longueurs permettent, entre autre, de détecter du bruit en chaque point du contour ainsi que l'échelle significative. Nous proposons d'étendre cette méthode à la détection de bruit local sur les contours discrets tridimensionnels. Pour cela, nous nous orientons vers une analyse multi-échelle des plans discrets maximaux couvrant chaque point du contour. Nous choisissons dans un premier temps d'étudier le critère de l'aire discrète et nous espérons observer un comportement asymptotique caractéristique. Ces travaux sont actuellement en cours.

Thursday 23rd September 2010 at 10h07 Laurent Vuillon (LAMA),
Mots infinis obtenus par clôtures palindromique et antipalindromique

Abstract: (Hide abstracts)
Dans cet exposé, nous allons présenter un outil important pour la construction des mots de Sturm (et donc également pour les droites discrètes) que l'on nomme la clôture palindromique. Nous allons étendre cette notion pour atteindre des mots infinis comme les mots de Rote ou encore la fameuse suite de Thue-Morse. Enfin, nous montrerons comment calculer les diverses clôtures d'une façon efficace.

Thursday 16th September 2010 at 10h Tom Hirschowitz (LAMA),
Cartesian closed 2-categories and higher-order rewriting

Abstract: (Hide abstracts)
Notions of cartesian closed sketches have been proposed as a categorical approach to algebra with binding. We here consider a 2-dimensional refinement of this idea, called cartesian closed 2-signatures, as a categorical approach to higher-order rewriting, i.e., rewriting with variable binding. We sketch a general notion of standardisation in the sense of Lévy (1980).

Tuesday 20th July 2010 at 10h Martin Delacourt (LIF, Marseille),
Directional dynamics along arbitrary curves on cellular automata of dimension 1

Abstract: (Hide abstracts)
Cellular automata are both a powerful model of computation and a continuous function on a Cantor space. So the notion of equicontinuity is naturally defined, and corresponds to the ability to block any communication. This property is most of the time considered along the line (x=0). Mathieu Sablik extended it first to all lines, and here we want to deal with automata that are equicontinuous along any curve. I’ll present a classification of cellular automata considering it, with examples, and some dynamical consequences.

Tuesday 8th June 2010 at 10h Florian Hatat (LAMA),
Un jeu graphique pour les catégories de réponse

Abstract: (Hide abstracts)
Dans cet exposé, on s'intéresse aux catégories de réponse (des catégories avec les produits finis et un objet exponentiel, introduites par Selinger) sous deux aspects : La composition usuelle des catégories provient de deux propriétés du jeu graphique : Le but est d'ébaucher une structure triple-catégorique pour décrire un langage de programmation, et de voir :

Tuesday 25th May 2010 at 13h30 Aline Parreau (Institut Fourier),
Identifier les sommets d'un graphe avec des couleurs

Abstract: (Hide abstracts)
Dans cet exposé, nous cherchons à colorier proprement des graphes de sorte que deux sommets adjacents n'aient pas le même ensemble de couleurs dans leur voisinage fermé. On peut par exemple colorier de cette manière n'importe quel graphe biparti avec 4 couleurs, mais savoir si l'on peut colorier un graphe biparti avec seulement 3 couleurs est NP-complet. Nous nous interesserons aussi à une autre classe de graphes : les graphes triangulés pour lesquels nous pensons que 2*k couleurs sont suffisantes, avec k la taille de la plus grande clique. Enfin, je donnerai des relations avec le nombre chromatique et avec le degre maximum du graphe.

Thursday 20th May 2010 at 10h Alexandre Miquel (ENS Lyon),
Une analyse du contenu calculatoire de la transformation de preuve par la méthode de forcing

Abstract: (Hide abstracts)
Dans cet exposé (très largement inspiré des travaux de Krivine présentés en juin dernier), je propose d'étudier à travers la correspondance de Curry-Howard la transformation de preuves sous-jacente à la méthode de forcing. Pour cela, je me placerai en arithmétique d'ordre supérieur (PAw) avec termes de preuves à la Curry. Je définirai d'abord la transformation qui à une proposition A associe la proposition p ||- A (où p est une condition arbitraire), puis une transformation t |-> t^* sur les termes de preuves bruts (i.e. non typés) telle que si t : A, alors t^* : p ||- A. Je montrerai alors comment le terme traduit effectue ses calculs, et en quoi il est légitime de voir cette transformation comme la mise en place d'un petit système d'exploitation.

Thursday 29th April 2010 at 10h Olivier Laurent (ENS Lyon),
Jeux et realisabilite

Abstract: (Hide abstracts)
En s'inspirant de certaines constructions de la ludique, on definit une realisabilite par orthogonalite pour la semantique des jeux de la logique lineaire intuitionniste. On demontre ainsi, sans passer par l'elimination des coupures, que l'interpretation d'une preuve (y compris avec coupures) est une strategie totale (analogue de la terminaison dans les jeux).

Thursday 8th April 2010 at 10h Muhammad Humayoun (LAMA),
Towards Automatic Formalisation of Informal Mathematical Text

Abstract: (Hide abstracts)
Can we build a program that understands informal mathematical text and can we mechanically verify it's correctness? MathNat project aims at being a first step towards answering this question. We develop a controlled language for mathematics (CLM), which is a precisely defined subset of English with restricted grammar and dictionary. Like textbook mathematics, CLM supports some complex linguistic features to make it natural and expressive. A number of transformations are further applied on it to completely formalise it. In this presentation, I'll give an overview of this work and report the current state and future directions. Web: humayoun/phd/mathnat.html

Thursday 25th March 2010 at 10h Luc Gillibert (Centre de Morphologie Mathématique de l'Ecole des Mines de Paris),
Une approche géométrique pour la segmentation de la neige

Abstract: (Hide abstracts)
L'étude la microstructure des matériaux granulaires nécessite souvent de séparer numériquement les grains de leurs voisins. A cause d'effets thermodynamique et mécanique, toute couche de neige non fraîche est dégradée de différentes façons. Le principal problème est donc de choisir une définition géométrique d'un ``grain'' qui soit cohérente avec la physique et la mécanique de la neige. Les images microtomographiques au rayon X de la structure de la neige ne fournissent aucune information directe sur les frontières entre les grains. Pour résoudre ce problème, nous faisons appel à une approche basée sur la géométrie discrète. En travaillant sur la surface de la structure neigeuse, il est possible de calculer sa courbure Gaussienne et moyenne. Muni de ces informations, il devient possible de séparer la surface en deux régions. En utilisant un diagramme de Voronoi, ces régions sont étendues à l'objet entier. Les voxels dans la région négative sont retirés de l'image, fournissant ainsi une segmentation en objets déconnectés. Ces objets sont alors utilisés comme graines pour un second diagramme de Voronoi.

Tuesday 23rd March 2010 at 13h30 Laurent Provot (Loria),
Vers une polyédrisation des objets discrets bruités 3D

Abstract: (Hide abstracts)
Les travaux que je présenterai sont ceux effectués lors de ma thèse. Ils s'inscrivent dans le cadre de la géométrie discrète, une discipline ayant pour objectif de définir un cadre théorique pour transposer dans Z^n les bases de la géométrie euclidienne -- les notions discrètes définies étant le plus proche possible des notions continues que nous connaissons (telles que distance, droite, convexité, ...). De nombreuses études ont déjà été menées au sein de cette discipline, pour en définir l'espace de travail ainsi que les objets fondamentaux manipulés et en saisir leurs propriétés. Des algorithmes de reconnaissance pour ces primitives discrètes ont été développés et utilisés dans des problèmes comme la reconnaissance de formes, l'extraction de caractéristiques géométriques et bien d'autres encore. Néanmoins, la majorité des études ont été effectuées en se reposant sur la régularité des structures fondamentales de l'espace discret, souvent issues de définitions arithmétiques, et ces critères de régularité sont généralement essentiels aux différents algorithmes développés. Or, en pratique, les objets manipulés sont très souvent bruités par les méthodes d'acquisition (scanners, IRM, ...) qui suppriment ce caractère régulier des objets. Dans cet exposé, nous nous intéressons aux objets discrets 3D et proposons une primitive discrète, le morceau flou de plan discret, destinée à apporter plus de flexibilité dans les traitements, afin de concevoir des algorithmes capables de fournir des résultats satisfaisants aussi bien sur des objets réguliers que non réguliers. Avec l'emploi de cette nouvelle primitive discrète, nous définissons différents estimateurs de caractéristiques géométriques au bord d'objets discrets et montrons comment les utiliser dans des problèmes de segmentation et de polyédrisation d'objets discrets possiblement bruités.

Tuesday 23rd March 2010 at 10h15 Dobrina Boltcheva (Inrialpes),
Modélisation géométrique et topologique d'images 3D

Abstract: (Hide abstracts)
Je vais vous présenter mes activités de recherche de thèse et de post-doc qui peuvent être regroupées sous le thème général de la modélisation géométrique et topologique. En particulier, je me suis intéressée au problème de la génération de maillages surfaciques et volumiques à partir d'images 3D multi-labels.

Thursday 18th March 2010 at 10h Xavier Provençal (LIRMM et LAMA),
Convexité discrète et combinatoire des mots

Abstract: (Hide abstracts)
L'étude de la combinatoire des mots a mené à la caractérisation de nombreux langages. Certains admettent (ou sont fondés sur) une interprétation géométrique. En particulier, une condition nécessaire et suffisante à la convexité discrète s'énonce en termes de mots de Lyndon et de Christoffels. À partir de cette caractérisation, vient naturellement la notion de convexité minimale. Ces ``mots non-convexes minimaux'' possèdent une structure combinatoire particulière et sont reliés aux MLP (minimum length polygon).

Tuesday 16th March 2010 at 10h Jérôme Hulin (LaBRI, Bordeau),
Voisinage de test pour le calcul de l'axe médian discret

Abstract: (Hide abstracts)
L'axe médian est un outil de représentation d'objets binaires par ensemble de boules, et est couramment utilisé en analyse d'images. Soit (E,d) un espace métrique, et S une forme binaire incluse dans E. Une boule B (pour la distance d) est dite maximale dans S si elle est incluse dans S mais n'est incluse dans aucune autre boule incluse dans S. L'Axe Médian de S est défini comme l'ensemble des boules maximales de S [Blum 67, Pfaltz et Rosenfeld 67]. Nous présentons plusieurs nouveaux résultats concernant le calcul de l'axe médian, dans le cas de la géométrie discrète (E=Z^n), pour la distance euclidienne et les normes de chanfrein (discrétisation dans Z^n des jauges polyédrales). Nous procédons par recherche locale : nous donnons des caractérisations de voisinages de test suffisants pour calculer l'axe médian. Nous verrons comment ces voisinages dépendent de la distance considérée, ainsi que de l'épaisseur de la forme étudiée. En particulier, nous établissons des liens avec des outils bien connus de l'arithmétique, tels que les suites de Farey et le problème de Frobenius.

Wednesday 10th March 2010 at 13h15 Diane Larlus (Technische Universität, Darmstadt),
Segmentation de catégories d'objets, par combinaison d'un modèle par sac-de-mots et d'un champ de Markov

Abstract: (Hide abstracts)
Dans cette présentation, nous nous intéressons à la segmentation d'images, et plus particulièrement à la segmentation de catégories d'objets. Si les modèles d'apparence par sac-de-mots donnent à ce jour les meilleures performances en terme de classification d'images et de localisation d'objets, ils ne permettent pas de segmenter précisément les frontières des objets. Parallèlement, les modèles basés sur des champs de Markov (MRF) utilisés pour la segmentation d'images se basent essentiellement sur les frontières et permettent une régularisation spatiale, mais utilisent difficilement des contraintes globales liées aux objets, ce qui est indispensable lorsqu'on travaille avec des catégories d'objets dont l'apparence peut varier significativement d'une instance à l'autre. Nous verrons comment combiner ces deux approches. Notre approche comporte un mécanisme basé sur la détection d'objets par sac-de-mots qui produit une segmentation grossière des images, et simultanément, un second mécanisme, lui basé sur un MRF, produit des segmentations précises. Notre approche est validée sur plusieurs bases publiques de référence, contenant différentes classes d'objets en présence de fonds encombrés et présentant de larges changements de points de vue.

Tuesday 9th March 2010 at 10h Alexis Ballier (LIF, Marseille),
Ordonnons les pavages

Abstract: (Hide abstracts)
Je présenterai deux ordres que l'on peut définir sur les pavages: un premier basé sur la dérivée topologique (le rang de Cantor-Bendixson) et un second plus combinatoire basé sur les motifs que l'on peut trouver dans un pavage. Ces deux ordres, étudiés indépendamment, permettent d'obtenir des propriétés sur les ensembles de pavages. Nous verrons comment combiner les deux pour obtenir des résultats plus précis: sous l'hypothèse de n'avoir qu'une infinité dénombrable de pavages possibles nous arrivons à montrer qu'il existe des pavages n'ayant qu'une seule direction de périodicité; nous arrivons aussi à caractériser les ensembles de pavages ayant la cardinalité du continu.

Thursday 4th March 2010 at 10h Benno van den Berg (Technische Universität Darmstadt),
Introduction to Algebraic Set Theory

Abstract: (Hide abstracts)
Algebraic set theory was introduced by Joyal and Moerdijk in their book from 1995 and is an approach to the semantics of set theory based on categorical logic. One of its strengths is that it gives a uniform approach to set theories of different kinds (classical and constructive, predicative and impredicative). In addition, it allows one to capture different kinds of semantics (forcing, sheaves, boolean-valued models, realizability) in one common framework. In this talk, I will give an introduction to the subject, concentrating on main ideas rather than technical details.

Thursday 25th February 2010 at 14h Alexandre Miquel (LIP, ENS Lyon),
Forcing et négation de l'hypothèse du continu

Abstract: (Hide abstracts)
Dans les cours précédents, nous avons construit le modèle booléen V^B de ZF et montré la satisfaction des axiomes de ZFC. Dans cette ultime séance de cours, nous allons nous intéresser aux cardinaux dans le modèle, et construire un modèle réfutant l'hypothèse du continu. Au programme: condition de (anti-)chaîne dénombrable, ensemble de conditions, forcing et modèles booléens, réels de Cohen.

Thursday 25th February 2010 at 10h Alberto Dennunzio (FISLAB, Università di Milano-Bicocca, Italy),
Automates Cellulaire 2D : constructions et dynamique

Abstract: (Hide abstracts)
Les automates cellulaires (AC) sont des systèmes dynamiques à temps et espace discret. Ils sont l'un des modèles formels les plus utilisés pour étudier des systèmes complexes. Bien que les applications concernent principalement les AC en dimension 2 ou supérieure, les études formelles ont été menées surtout en dimension 1. Dans cet exposé je présente des résultats sur la dynamique des AC en dimension 2. Ces résultats sont obtenus par deux constructions qui permettent de considerer un AC en dimension 2 comme un AC en dimension 1.

Friday 12th February 2010 at 10h15 Andreas Abel (INRIA et LMU Munich),
Normalization by Evaluation for Dependent Type Theory (work in progress)

Abstract: (Hide abstracts)
Normalization by Evaluation (NbE) is an abstract framework for computing the full normal form of lambda-terms through an interpreter, just-in-time compiler or an abstract machine. While computational equality such as beta is part of every dependent type theory, the status of extensional laws such as eta is less clear. The reason is that eta needs a typed equality but many type theories (like Pure Type Systems) are formulated with untyped equality in order to decide equality by rewriting.
In this talk, I am arguing that NbE is the tool of choice to implement typed beta-eta equality for dependent type theory. I present typed NbE which computes eta-long normal forms, and show how to construct a model of (possibly impredicative) type theory that proves the correctness of NbE. Hence, NbE can be used to decide the built-in (``definitional'') equality of type theory with eta-rules.
The aim of this work is to provide foundational justifications of powerful type theories with beta-eta equality, such as the Calculus of Inductive Constructions.

Tuesday 9th February 2010 at 10h Tristan Roussillon (LIRIS, Lyon),
Algorithmes d'extraction de modèles géométriques discrets pour la représentation robuste des formes

Abstract: (Hide abstracts)
Ce travail se situe à l'interface entre l'analyse d'images, dont l'objectif est la description automatique du contenu visuel, et la géométrie discrète, qui est l'un des domaines dédiés au traitement des images numériques. Dans ce cadre, nous avons considéré les régions homogènes et porteuses de sens d'une image, avec l'objectif de représenter leur contour au moyen de modèles géométriques ou de les décrire à l'aide de mesures. Nous nous sommes concentrés sur trois modèles géométriques discrets définis par la discrétisation de Gauss : la partie convexe ou concave, l'arc de cercle discret et le segment de droite discrète. Nous avons élaboré des algorithmes dynamiques (mise à jour à la volée de la décision et du paramétrage), exacts (calculs en nombres entiers sans erreur d'approximation) et rapides (calculs simplifiés par l'exploitation de propriétés arithmétiques et complexité en temps linéaire) qui détectent ces modèles sur un contour. L'exécution de ces algorithmes le long d'un contour aboutit à des décompositions ou à des polygonalisations réversibles. De plus, nous avons défini des mesures de convexité, linéarité et circularité, qui servent à l'introduction de nouveaux modèles dotés d'un paramètre variant entre 0 et 1. Le paramètre est fixé à 1 quand on est sûr de la position du contour, mais fixé à une valeur inférieure quand le contour est susceptible d'avoir été déplacé par un bruit d'acquisition. Cette approche pragmatique permet de décomposer de manière robuste un contour en segments de droite ou en parties convexes et concaves.

Thursday 28th January 2010 at 13h30 Alexandre Miquel (LIP, ENS Lyon),
La construction du modèle booléen de ZF (suite)

Abstract: (Hide abstracts)
Cette séance est consacrée au modèle booléen V^B de ZF, dont la construction est paramétrée par une algèbre de Boole complète B dans le modèle initial. Au programme: rappels de théorie des ensembles (classes et hiérarchie de Veblen), définition de la hiérarchie des B-ensembles, effondrement extensionnel, mélange de B-ensembles, principe du maximum et plénitude, conservation des propriétés Sigma_1, satisfaction des axiomes de ZFC.

Thursday 28th January 2010 at 10h15 Christian Mercat (I3M, Montpellier),
Géométrie discrète conforme

Abstract: (Hide abstracts)
Je présenterai ce qu'est une paramétrisation conforme d'une surface et son intérêt pour la géométrie discrète, en particulier la géométrie digitale, pour le plaquage de texture et le calcul des grandeurs géométriques d'une surface ou d'une courbe (normale, courbure...). Je discuterai de diffusion discrète, du laplacien discret dans le cadre des maillages et dans le cadre voxellique. La théorie de l'analyse conforme discrète qui est associée partage de nombreux points avec la théorie des surfaces de Riemann continue.

Tuesday 19th January 2010 at 10h15 Nicolas Ollinger (LIF, Marseille),
L'indécidable périodicité des automates cellulaires

Abstract: (Hide abstracts)
Les automates cellulaires ont cette riche dualité de pouvoir être à la fois considérés comme des systèmes dynamiques à temps et espace discret et comme des objets combinatoires simples proches des modèles de calcul de type machine. Cette dualité permet d'établir facilement des résultats de calculabilité et de complexité concernant la dynamique de ces objets. Dans cet exposé, nous abordons une propriété dynamique élémentaire : l'existence d'une période temporelle commune à toutes les configurations du système. Sans surprise, nous établissons l'indécidabilité de cette propriété. Pour établir ce résultat, les outils maintenant classiques liant pavages et automates cellulaires ne fonctionnent pas. C'est donc l'occasion d'exhiber de nouveaux outils adaptés et de redécouvrir d'anciens résultats sur les machines de Turing. Nous aborderons les notions de mortalité et de périodicité dans ce modèle de calcul, l'art et la manière de programmer dans un cadre réversible et nous montrons que le problème de l'immortalité des machines de Turing reste indécidable dans le cadre réversible. Ces travaux sont issus d'une collaboration avec J. Kari (Univ. Turku, Finlande)

Thursday 14th January 2010 at 10h Damien Regnault (LIF, Marseille),
Minorité stochastique sur les pavages par coupe et projection: application à la formation des quasi-cristaux

Abstract: (Hide abstracts)
Cet exposé commence par la présentation rapide de la règle Minorité stochastique et de ses particuliarités. Ensuite, je présenterai une application de cette règle pour modéliser la formation de quasi-cristaux.
Considérons un graphe où chaque sommet reçoit la couleur noire ou blanche. Une arête contient une erreur si elle relie deux sommets de la même couleur. Minorité est une dynamique stochastique minimisant rapidement l'énergie. Sous cette dynamique, un sommet, chosi aléatoirement et uniformément parmi l'ensemble des sommets, peut changer d'état si au moins la moitié des arêtes qui lui sont adjacentes sont erronées. Cette dynamique est sensible à la topologie du graphe et son analyse fine s'est révélée compliquée.
En physique, dans les annnées 70, il était conjecturé que toutes les structures ordonnées soient périodiques. En 1984, un contre-matériaux fût découvert et reçu le nom de quasi-cristal. Dès 1974, Penrose avait présenté un structure théorique ordonnée et apériodique. Le but de notre projet est de présenter un modèle pour expliquer la formation d'une telle structure. Pour cela, nous considérons le modèle des pavages par coupe et projection (qui contient le pavage de Penrose). En définissant une notion d'erreur et d'énergie sur ces pavages, la règle Minorité procédant par flips permet de converger rapidement expérimentalement vers une structure ordonnée qui selon la famille de pavages par coupe et projection considérée est soit périodique, soit apériodique. Je présenterai nos résultats expérimentaux ainsi que notre analyse de cette dynamique pour les pavages 2 vers 1 (mots sur deux lettres).

Tuesday 12th January 2010 at 14h Antoine Vacavant (LIRIS, Université Lumière Lyon 2),
Géométrie discrète sur grilles irrégulières isothétiques

Abstract: (Hide abstracts)
Les systèmes d'acquisition de données image en deux ou trois dimensions fournissent généralement des données organisées sur une grille régulière, appelées données discrètes. Que ce soit pour la visualisation ou l'extraction de mesures, la géométrie discrète définit les outils mathématiques et géométriques pour de nombreuses applications. Dans cet exposé, je présenterai comment adapter divers algorithmes de la géométrie discrète aux grilles irrégulières isothétiques. Ce modèle de grille permet de représenter de manière générique les structurations d'images en pixels ou voxels de taille et de position variables : les grilles anisotropes, très répandues en imagerie médicale, les décompositions hiérarchiques telles que quadtree/octree, les techniques de compression comme le run length encoding, etc. Plus précisément, je présenterai l'extension à cette représentation de plusieurs méthodologies largement étudiées pour analyser les formes discrètes: la reconstruction d'objets binaires complexes, la transformée en distance et l'extraction d'un axe médian. Je montrerai enfin comment ces outils sont employés dans diverses applications : la distinction de caractères ambigus dans un outil de reconnaissance de plaques minéralogiques, l'approximation dynamique de courbes implicites planaires et l'analyse d'objets discrets bruités.

Thursday 7th January 2010 at 13h30 Alexandre Miquel (LIP, ENS Lyon),
La construction du modèle booléen de ZF

Abstract: (Hide abstracts)
Cette séance est consacrée au modèle booléen V^B de ZF, dont la construction est paramétrée par une algèbre de Boole complète B dans le modèle initial. Au programme: rappels de théorie des ensembles (classes et hiérarchie de Veblen), définition de la hiérarchie des B-ensembles, effondrement extensionnel, mélange de B-ensembles, principe du maximum et plénitude, conservation des propriétés Sigma_1, satisfaction des axiomes de ZFC.

Thursday 7th January 2010 at 10h15 Gavin Seal (EPFL),
Des ensemble ordonnés aux espaces topologiques

Abstract: (Hide abstracts)
Parmi les nombreuses structures ordonnées liées aux espaces topologiques, les treillis continus occupent une place importante. Ils constituent par exemple les espaces topologiques de Kolmogorov injectifs. Nous nous proposons ici de présenter ces treillis d'un point de vue algébrique au travers de la notion de monade et d'adjonction de Galois. La définition originelle d'espace topologique donnée par Hausdorff en 1914 apparaît alors de façon naturelle, et nous permet de jeter un regard neuf sur le résultat d'injectivité mentionné ci-dessus.

Thursday 17th December 2009 at 10h Séminaire Choco (Plusieurs orateurs),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 10th December 2009 at 10h15 Laurent Boyer (LAMA),
Factor universality in cellular automata

Abstract: (Hide abstracts)

Thursday 3rd December 2009 at 10h15 Krzysztof Worytkiewicz (AGH University of Science and Technology),
Une structure de modeles ``folk'' pour les omega-categories

Abstract: (Hide abstracts)
Nous construisons une structure de modeles de Quillen pour la categorie des omega-categories strictes, a partir d'un ensemble de cofibrations generatrices et d'une classe d'equivalences faibles. Toute omega-categorie est fibrante par rapport a cette structure, alors que les omega-categories cofibrantes sont precisement les libres.

Thursday 19th November 2009 at 10h15 Jean-Marc Andréoli (Xerox Research Centre Europe),
Deux digressions autour de la logique linéaire

Abstract: (Hide abstracts)
Cet exposé est divisé en deux parties distinctes présentant deux sujets de recherche autour de la Logique Linéaire. Bien qu'abordés il y a longtemps, ces sujets présentent toujours des questions ouvertes intéressantes. L'exposé pose plus de questions qu'il ne donne de réponses.
Le premier sujet concerne la notion de structure en Logique Linéaire. De nombreuses extensions de la Logique Linéaires ont été proposées dans le passé pour introduire une forme de structure qui dépasse celle de multi-ensemble: logique cyclique, logique non commutative, calcul de Lambek non associatif (qui en fait prédate la Logique Linéaire)... Un cadre général, appelé ``Logiques Linéaires Colorées'', a été proposé pour capturer les mécanismes communs à toutes ces extensions, et permettant d'en construire d'autres à l'infini, respectant automatiquement les propriétés essentielles d'élimination de la Coupure et de focalisation (ce travail montre d'ailleurs que ces deux propriétés sont intimement liées). La question ouverte est de comprendre quels critères supplémentaires permettent de séparer, dans cette infinité potentielle de systèmes, le bon grain de l'ivraie, avec l'idée sous-jacente que la Logique devrait avoir un caractère de nécessité, et ne pas laisser place à l'arbitraire.
Le deuxième sujet concerne un paradigme de programmation fondé non pas sur la réduction des coupures dans les réseaux de preuves mais sur la construction de réseaux de preuves en Logique Linéaire. La construction de réseaux, comme la réduction, peut se faire en parallèle, mais, contrairement à la réduction, il y a des séquentialisations irréductibles, qu'exprime la nécessité de respecter le critère de correction. Le paradigme résultant est très proche de celui, plus pragmatique, des systèmes transactionnels, issus du monde des bases de données, mais dont les mécanismes sont aujourd'hui présents dans les couches intergicielles de toutes les grandes applications réparties. Un mécanisme de construction incrémental de réseaux de preuves a été proposé dans le passé dans le cadre du fragment strictement multiplicatif de la Logique Linéaire. Les questions ouvertes sont ici de savoir si ce mécanisme est optimal pour le fragment visé d'une part et d'autre part s'il peut être étendu à des fragments plus larges, voire au système complet.

Thursday 12th November 2009 at 14h Groupe de lecture Kohlenbach (Plume et LIMD),
Séance 2

Abstract: (Hide abstracts)
Deuxième séance du groupe de lecture sur le livre de Kohlenbach ``Applied Proof Theory''.

Thursday 12th November 2009 at 10h15 Vasileios Koutavas (Trinity College, Dublin),
First-Order Reasoning about Higher-Order Concurrency

Abstract: (Hide abstracts)
Developing effective reasoning techniques for languages with higher- order constructs is a challenging problem, made even more challenging with the presence of concurrency and mobility. In this talk I will present a practical and effective reasoning methodology for such a language, which employs first-order reasoning and handles examples in a straightforward manner. There are two significant aspects to this theory. The first is that higher-order inputs are treated in a first- order manner, hence eliminating the need to reason about arbitrarily complicated higher-order contexts, or to use up-to context techniques, when establishing equivalences between processes. The second is that we use augmented processes to record directly the knowledge of the observer. This has the benefit of making ordinary first-order weak bisimulation fully abstract w.r.t. contextual equivalence. It also simplifies the handling of names, giving rise to a truly propositional Hennessy-Milner characterisation of higher-order contextual equivalence. I will illustrate the simplicity of the approach with example equivalences and inequivalences, and use it to show that contextual equivalence in a higher-order setting is a conservative extension of the first-order pi-calculus.

Thursday 5th November 2009 at 10h15 Alexandre Miquel (LIP, ENS Lyon),
Modèles booléens (II)

Abstract: (Hide abstracts)
La séance précédente était consacrée aux algèbres de Boole et aux notions de filtre, d'idéal et d'ultrafiltre. Cette séance sera consacrée à la définition de la notion de modèle Booléen (en insistant sur les problèmes soulevés par cette définition) et à l'étude de ses propriétés: validité, complétude, etc. Je présenterai les principales constructions attachées aux modèles booléens: produit, quotient, ultraproduit, ultrapuissance. Je terminerai en montrant comment la théorie peut être appliquée à la construction des modèles de l'analyse non standard.

Thursday 22nd October 2009 at 10h Séminaire Choco (Plusieurs orateurs),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 15th October 2009 at 10h15 Matthieu Simonet (LAMA),
Mots de retour et pavage dans les plans discrets

Abstract: (Hide abstracts)
En combinatoire des mots et plus précisément dans l'étude des mots unidimensionnels, la notion de mot de retour a joué un rôle important, en particulier dans la caractérisation des mots sturmiens. Ces mots servant de représentation pour les droites discrètes, il est tout naturel de se poser la question d'une caractérisation en dimension supérieure, en particulier dans le cas des plans discrets. En dimension 2, on vient à considérer des mots bidimensionnels. Les notions habituelles doivent donc être adaptées. Nous verrons que le passage à la dimension 2 provoque de vrais problèmes vis à vis de définitions simples en dimension 1.

Thursday 8th October 2009 at 10h15 Karim Nour (LAMA),
Un lambda-calcul parallèle

Abstract: (Hide abstracts)
Je présente un lambda calcul codant une logique intuitionniste du second ordre et permettant de programmer un ``ou-parallèle''. Ce calcul a les propriétés suivantes : ``préservation de type'', ``forte normalisation'' et ``unicité de représentation des données''. Il permet aussi d'écrire des programmes avec une sorte d'exception. Il est inspire du lambda-mu-{++}-calcul que j'ai introduit en 2002.

Thursday 1st October 2009 at 14h Alexandre Miquel (LIP, ENS Lyon),
Une introduction aux modèles booléens

Abstract: (Hide abstracts)
En 1962, Cohen a résolu le premier problème de Hilbert en montrant que l'hypothèse du continu est indécidable dans la théorie des ensembles de Zermelo-Fraenkel. La technique qu'il a introduite pour établir ce résultat non trivial - le forcing - est devenue aujourd'hui un outil standard en théorie des modèles. Cette technique a permis d'établir de nombreux autres résultats de cohérence relative (ou d'indépendance), comme par exemple la cohérence de l'axiome de Solovay: « toute partie de R est mesurable au sens de Lebesgue » dans une théorie des ensembles sans axiome du choix (mais avec choix dépendant).
Dans cet exposé introductif au forcing, je me propose de présenter la théorie des modèles booléens, une variante du forcing (introduite par Scott, Solovay et Vopenska dans les années 1960) qui permet de faire essentiellement les mêmes constructions que Cohen, mais dans un cadre qui est plus facile à saisir au premier abord. J'introduirai les notions de base (algèbres de Boole, ultrafiltres, modèles booléens, quotient, produit, ultraproduit et ultrapuissance) tout en illustrant mon propos par quelques exemples de constructions, notamment en lien avec l'« analyse non standard ».
La preuve de l'indépendance de l'hypothèse du continu à l'aide de ces outils fera l'objet de l'exposé suivant.

Thursday 24th September 2009 at 14h Martin Hofmann (LMU, Munich),
Amortized Resource Analysis with Polynomial Potential

Abstract: (Hide abstracts)
In 2003, Hofmann and Jost introduced a type system that uses a potential-based amortized analysis to infer bounds on the resource consumption of (first-order) functional programs. This analysis has been successfully applied to many standard algorithms but is limited to bounds that are linear in the length of the input.

Here we extend this system to polynomial resource bounds. An automatic amortized analysis is used to infer these bounds for functional programs without further annotations if a maximal degree for the bounding polynomials is given. The analysis is generic in the resource and can obtain good bounds on heap-space, stack-space and time usage. Furthermore, the analysis can be used to infer polynomial relations between the input and the output sizes of a function in the sense of sized types.

Travail en collaboration avec Jan Hoffmann.

Thursday 24th September 2009 at 10h15 Pawel Sobocinski (Southampton),
An introduction to the wire calculus

Abstract: (Hide abstracts)
The wire calculus is a process algebra for modelling truly concurrent systems with explicit network topologies. It benefits from using categorical operators for coordination of processes: the tensor product and sequential composition of monoidal categories. The dynamics are handled by operators inspired by Milner's CCS and Hoare's CSP: unary prefix operation, binary choice and a standard recursion construct. The operational semantics is a labelled transition systems derived using SOS rules. After presenting the formal definition of the calculus I will discuss some basic results and give several examples.

Friday 18th September 2009 at 08h45 Emilie Charrier (LAMA),
Cocktail de géométrie discrète :
Approximation de nombres réels par des rationnels à dénominateur borné
Reconnaissance de plans discrets
Épaisseur dans un réseau n-dimensionnel

Abstract: (Hide abstracts)
Les différentes parties de mes travaux de thèse en géométrie discrète et géométrie algorithmique seront présentées durant cet exposé.

Partie 1 : Nous considérons tout d’abord le problème de l’approximation d’un nombre réel par un nombre rationnel de dénominateur borné. Soit a un nombre réel, soit b et b’ deux nombres entiers tels que b
Partie 2 : Par la suite, nous présenterons notre algorithme de reconnaissance de plans discrets. Nous rappelons qu’un ensemble de points S de Z^3 est appelé morceau de plan discret s’il est contenu dans la discrétisation d’un plan euclidien. Un tel algorithme est utilisé pour décider si un sous-ensemble de points d’un objet discret peut être remplacé par une facette dans une représentation polyédrique de l’objet. La méthode proposée décide si un sous-ensemble de points de Z^3 correspond à un morceau de plan discret en résolvant un problème de réalisabilité sur une fonction convexe en dimension 2, dite fonction épaisseur. Ainsi, notre méthode ne prend en compte que deux paramètres et elle utilise des techniques géométriques planaires pour déterminer si l’espace des solutions est vide. Notre algorithme s’exécute en O(n log D) dans le pire cas ou n correspond au nombre de points de l’ensemble S et D représente la taille d’une boite englobant S. Notre méthode s’avère également efficace en pratique et reconnaît un ensemble de 10^6 points en environ 10 itérations linéaires.

Partie 3 : Si le temps nous le permet, nous aborderons enfin une problématique un peu à part : calculer l’épaisseur d’un ensemble de points de Z^d dans le réseau entier de même dimension (épaisseur latticielle). L’épaisseur d’un ensemble de points K suivant une direction c de Z^d correspond à la quantité max{c.x | x \in K} - min{c.x | x \in K}. L’épaisseur latticielle de l’ensemble de points K correspond à l’épaisseur minimum pour toutes les directions du réseau. D’après une idée originale de Fabien FESCHET, nous avons mis en place un algorithme valable en toute dimension pour déterminer cette épaisseur. Cette méthode s’avère optimale puisque linéaire en temps dans le cas planaire. En dimensions supérieures, nous passons par une approche gloutonne qui s’avère efficace en pratique.

Abstract available as a PDF file.

Thursday 10th September 2009 at 14h Mark Weber (MPI Bonn),
TBA (On funny tensor products)

Abstract: (Hide abstracts)

Thursday 10th September 2009 at 10h15 Christophe Raffalli (LAMA),
PML pour les nuls

Abstract: (Hide abstracts)
L'exposé sera pour un public de non spécialistes. J'essaierai de raconter ce qu'est un bon langage de programmation (selon moi) et donc ce qu'est PML. J'essaierai notamment d'expliquer les points suivants: Comme on aura pas le temps de tout faire... prévoir une suite (toujours pour un public de non spécialistes).

Thursday 27th August 2009 at 10h15 Pierre-Etienne Meunier (LAMA),
Complexité de communication et automates cellulaires

Abstract: (Hide abstracts)
Je ferai un premier exposé de complexité de communication, et un deuxième sur nos résultats sur les applications entre cette théorie et les automates cellulaires. Il y aura un peu de machines de Turing, pas mal d'automates cellulaires, beaucoup de complexité de communication, et aussi des circuits logiques. La complexité de communication est une théorie très générale, et il y a plein d'applications en complexité (parallèle et séquentielle), mais aussi des choses plus appliquées comme le design de processeurs, des problèmes de graphes, etc. En plus, c'est un modèle de calcul qui n'a pas besoin de la thèse de Church.

Thursday 16th July 2009 at 10h15 Alexandre Blondin Massé (LAMA),
Palindromes généralisés, chemins de Fibonacci et doubles pavages

Abstract: (Hide abstracts)
Dans cet exposé, je présenterai une famille de polyominos appelés doubles carrés, ayant la propriété de paver le plan par translation de deux façons distinctes. Rappelons qu'un polyomino est un sous-ensemble de la grille discrète qui est 4-connexe (connecté verticalement et horizontalement) et sans trou (c'est-à-dire que son complément est également 4-connexe). Nous pouvons en particulier coder son contour par un mot sur un alphabet à quatre lettres {h, b, g, d} codant les déplacements 'haut', 'bas', 'gauche' et 'droite'. J'introduirai d'abord les définitions de la combinatoire des mots nécessaires à cet exposé ainsi que les notions de polyominos et de pavages. Ensuite, je survolerai rapidement les résultats connus et certaines conjectures intéressantes. J'enchaînerai en présentant quelques propriétés sur les chemins liées à une généralisation de la notion de palindrome et je terminerai en présentant une famille de tuiles liées à la suite de Fibonacci. L'exposé se déroulera en québécois...

Thursday 25th June 2009 at 10h15 Sylvain Hallé (University of California Santa Barbara),
Le runtime monitoring d'une logique temporelle: une application aux contrats d'interface des applications web

Abstract: (Hide abstracts)
Des entreprises comme Amazon, Google et Yahoo rendent maintenant disponibles une partie de leurs fonctionnalités sous la forme de services web; une application tierce peut communiquer avec ces services via Internet en échangeant des messages dont la structure et le contenu sont publics et formellement définis. Cependant, la documentation précise également une foule d'autres détails sur la manière dont ces services doivent être consommés, exprimés en langue naturelle et échappant à toute formalisation. Ce contexte nous a amené à développer LTL-FO+, une extension de la logique temporelle LTL incluant 1) une forme particulière de quantification du premier ordre; 2) une sémantique à 2, 3 ou 4 valeurs de vérité, selon le contexte. On verra que, contrairement à LTL, elle est appropriée pour exprimer des contraintes sur les séquences de messages propres aux applications web. On s'intéressera par la suite à son runtime monitoring; pour ce faire, nous présenterons BeepBeep, un outil permettant la vérification et l'application de formules LTL-FO+ en temps réel sur de vraies applications web. Finalement, on verra au moyen d'un exemple concret (si la connexion Internet le permet) comment BeepBeep: 1) empêche une application web mal programmée de commettre des erreurs; et 2) nous permet de découvrir que les services web d'Amazon ne respectent pas certains détails de leur propre documentation.

Monday 18th May 2009 at 14h Alejandro Díaz-Caro (LIG),
Vectorial System F: Towards a Quantum Type System

Abstract: (Hide abstracts)
One of the purposes of quantum programming languages is to express quantum programs, however a possibly more important reason is to provide a framework for reasoning about the programs expressing quantum algorithms -- and hence about quantum computation in general.
Indeed, in classical computer science it is frequent to express the reasoning behind a program via several formally-defined logics. These logics provide important frameworks in which to reason and prove properties about the computational processes. Often they arise via the study of type systems for the language. Related to our motivation there is already a quantum logic, which was developed before quantum computing, and which is not known to have a clear relation to quantum programs and algorithms.
The Linear-Algebraic Lambda-Calculus extends the Lambda-Calculus with the possibility to make arbitrary linear combinations of terms a.t+b.u. We want to set up a type system for it which is capable of such handling vectorial notions, i.e. were types themselves form a vector space. This is needed at a practical level for instance in order to prove normalization and unitarity properties of terms. There is also the intriguing question as to what logical meaning we can give these `superposition types'.
Joint work with Pablo Arrighi.

Monday 18th May 2009 at 10h Pablo Arrighi (LIG),
Unitarity plus causality implies locality

Abstract: (Hide abstracts)
We consider a graph having a single quantum system sitting at each node. The entire compound system evolves in discrete time steps by iterating a global evolution G. Moreover we require that this global evolution G be unitary, in accordance with quantum theory, and that this global evolution G be causal, in accordance with special relativity. By causal we mean that information can only ever be transmitted at a bounded speed, the speed bound being quite naturally that of one edge of the underlying graph per iteration of G. We show that under these conditions the operator G is local; i.e. it can be put into the form of a quantum circuit made up with more elementary, unitary gates -- each acting solely upon neighbouring nodes.
Joint work with Vincent Nesme and Reinhard Werner.

Tuesday 12th May 2009 at 14h Types (2009),
Rencontre annuelle du projet Types

Abstract: (Hide abstracts)
Rencontre annuelle du projet Types, au centre Paul Langevin à Aussois, du 12 au 15 mai.

Thursday 7th May 2009 at 10h15 Guillaume Theyssier (LAMA),
Groupe de travail complexité géométrique

Abstract: (Hide abstracts)
Groupe de travail pour comprendre ce qu'on pourra de la théorie géométrique de la complexité à la Ketan Mulmuley. On se basera sur ses articles introductifs et les vidéos de ses conférences à l'Institute for Advanced Study en février 2009.

Thursday 30th April 2009 at 10h15 Damien Regnault (LIP, ENS Lyon),
Minorité stochastique sur les graphes

Abstract: (Hide abstracts)
Nous considérons un graphe où les cellules sont caractérisées par un état qui est soit noir, soit blanc. À chaque pas de temps, une cellule, choisie aléatoirement, se met à jour et passe dans l'état minoritaire dans son voisinage. L'évolution globale de ce processus ne semble pas dépendre de la topologie du graphe: dans un premier temps des régions, pavées par des motifs dépendant de la topologie du graphe, se forment rapidement. Puis dans un deuxième temps, les frontières entre ces régions évoluent jusqu'à devenir relativement stables. Nous étudions ce processus sous différentes topologies: arbres, anneaux, grilles, cliques. Ceci nous permet de montrer que même si ce processus se comporte à priori globalement de la même manière sur n'importe quel graphe, modifier la topologie influence la façon dont les régions sont pavées (rayures, damiers), la structure et les mouvements des frontières entre les régions, l'ensemble limite, le temps de relaxation (le temps nécessaire pour que le processus atteigne une configuration de l'ensemble limite). Ainsi, Minorité entraîne des comportements riches et variés qui se révèlent difficile à analyser. Comprendre cette règle simple est néanmoins nécessaire avant de considérer des règles plus compliquées.

Thursday 23rd April 2009 at 10h15 Guillaume Theyssier (LAMA),
Sous-shifts et logique monadique du second ordre

Abstract: (Hide abstracts)
Les mots (finis ou pas, en dimension 1 ou supérieure) peuvent être vus comme des modèles de formules de la logique monadique du second ordre (MSO), une formule définissant alors un langage. Cette approche a été suivie avec succès en dimension 1 par Büchi et Elgot dans les années 60 : les langages ainsi définis sont exactement les langages rationnels. De plus toute formule MSO est dans ce contexte équivalente à une formule EMSO (quantification existentielle au second ordre suivie d'une formule au premier ordre).
Plus récemment, Giammarresi, Restivo, Seibert et Thomas ont reconsidéré ces résultats dans le cas des ``figures'', c'est à dire des mots bidimensionnels finis avec bords marqués : cette fois les formules EMSO définissent exactement les langages ``sofiques'' (projections de langages locaux), mais elles ne suffisent plus à capturer tous les langages définissable par une formule MSO.
L'objectif de cet exposé est de développer cette approche, en dimension 2, pour les sous-shifts (ensembles de configurations fermés topologiquement et invariants par décalages). Nous verrons alors que les sous-shifts sofiques (introduits par Weiss dans les années 70) ne correspondent pas aux sous-shifts définissables par formules EMSO. Nous donnerons néanmoins une caractérisation logique des sous-shifts sofiques et, inversement, nous donnerons une caractérisation ``combinatoire'' des ensembles de configurations définissables dans EMSO.

Friday 3rd April 2009 at 08h45 Antonino Salibra (Venise),
Théories et Modèles du Lambda Calcul

Abstract: (Hide abstracts)
Je présente l'approche algébrique au lambda-calcul basée sur les algèbres de lambda abstraction et sur les algèbres de Boole, qui a permis d'étudier la structure du treillis des lambda théories et d'obtenir des résultats d'incomplétude pour le sémantique du lambda calcul. Depuis, je présente mon dernier résultat: la lambda théorie minimum extensionelle n'est pas la théorie d'une domaine de Scott réflexive.

Thursday 2nd April 2009 at 10h Choco (Ottawa, PPS et LIPN),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 26th March 2009 at 10h15 Assia Mahboubi (INRIA/MSR/LIX, Paris),

Abstract: (Hide abstracts)

Thursday 12th March 2009 at 10h Choco (TBA),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 5th March 2009 at 11h Pierre Clairambault (PPS, Paris 7),
Plus petits et plus grands points fixes en sémantique des jeux

Abstract: (Hide abstracts)
On montre comment trouver de façon naturelle des solutions à de nombreuses équations récursives en autorisant des boucles dans les arènes. On équipe ensuite les arènes de fonctions de gain et on s'intéresse aux stratégies totales et gagnantes. On présente alors deux fonctions de gain naturelles sur les arènes à boucles, qui premettent de construire respectivement des algèbres initiales et des coalgèbres finales à de nombreux endofoncteurs continus. Finalement on applique ces constructions pour donner un modèle correct (et complet, en un sens faible) d'un calcul des séquents intuitionniste, étendu par des constructions syntaxiques pour les plus petits et plus grands points fixes.

Thursday 26th February 2009 at 10h15 Alexandre Miquel (LIP, ENS Lyon),
Extraction de programmes à partir de preuves classiques en Coq

Abstract: (Hide abstracts)

Thursday 5th February 2009 at 10h15 Projet Choco (Lisbonne, LSV Cachan, PPS Paris 7),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 29th January 2009 at 10h15 Joachim Kock (Université de Barcelone),
Introduction to the theory of polynomial functors

Abstract: (Hide abstracts)
After defining polynomial functors and introducing their calculus in terms of certain bridge diagrams, I will survey some examples related to logic: Girard's normal functors, Jay and Cockett's shapely types, the containers of Abbott, Altenkirch and Ghani, multicategories after Lambek, Burroni, and Leinster, and finally trees. (This talk is based on a paper in preparation with Nicola Gambino.)

Thursday 22nd January 2009 at 10h15 Christophe Raffalli (LAMA),
Analyse grammaticale du français : des concepts théoriques ou de la bidoulle ?

Abstract: (Hide abstracts)
L'analyse de la langue naturelle est toujours un problème ouvert au sens où il n'a pas à ce jour d'outils disponible resolvant ce problème (qui est pourtant fini si l'on considère que la longueur des phrases est bornées par la plus longue phrase de Proust). Certaines approches reposent sur des concepts théoriques avancés (automates, théorie des types, jusqu'à MELL ou IMELL dans certains articles). Est-ce la bonne approche ? Ou bien juste le fait que l'algorithme est trop complexe pour être écrit à la main ? On va montrer que dypgen (Emmanuel Onzon) permet d'aller assez loin, sans toutefois analyser le présent résumé, en utilisant juste une juxtaposition d'idées au dessus des techniques récentes de parsing pour les grammaires hors contexte. Note: je n'expliquerai pas ce qu'il y a sous le capot de dypgen ... Pour ça, il faudra inviter Emmanuel Onzon.

Thursday 15th January 2009 at 10h15 François de Vieilleville (LAMA),
Segments maximaux et estimateurs de tangentes

Abstract: (Hide abstracts)

Thursday 18th December 2008 at 10h15 Mark Weber (PPS, Paris 7),
Monads with arities

Abstract: (Hide abstracts)
A ``monad with arities'' is a monad T on some category K together with some extra data expressing the basic ``shapes'' of the operations involved in the structure of a T-algebra. There is a general result, called the nerve theorem, which in the case where K is a presheaf category, shows that the notion of monad with arities is an efficient reformulation of the notion of ``limit sketch''. The nerve theorem is so named because it generalises the characterisation of the simplicial sets that arise as nerves of categories. Other interesting instances of this result relevant for higher dimensional algebra involve ``local right adjoint monads'' -- such a T comes with a canonical choice of arities. These examples formalise the passage between the operadic and simplicial approaches to higher category theory.

Thursday 11th December 2008 at 10h15 Geneviève Paquin (LAMA),
Etude des points fixes sous la fermeture pseudopalindromique itérative

Abstract: (Hide abstracts)
Parmi les nombreuses suites remarquables étudiées en combinatoire des mots figurent les suites sturmiennes. Elles interviennent dans plusieurs domaines: dynamique symbolique, géométrie discrète, astronomie, cristallographie, etc. Elles sont d'autant plus remarquables par le fait qu'elles possèdent plusieurs caractérisations équivalentes. Entre autres, elles décrivent les droites discrètes de pentes irrationnelles. Parmi ces droites, la classe des (demies) droites passant par l'origine, appelées des suites sturmiennes standards, admet une caractérisation supplémentaire: il est possible de les construire en utilisant la fermeture palindromique itérative. La fermeture palindromique d'un mot fini w consiste à trouver le mot palindromique le plus court ayant comme préfixe le mot w. La fermeture palindromique itérative d'un mot fini w, noté Pal(w), est définie par Pal(a)=a et Pal(w)=(Pal(w_0...w_{n-1})w_n)^+, où u^+ désigne la fermeture palindromique et a est une lettre de l'alphabet. Ainsi, à tout mot sur un alphabet à 2 lettres, on peut lui associer une suite sturmienne standard en appliquant l'opérateur de fermeture palindromique itérative. Plus récemment, cette notion a été généralisée à des pseudopalindromes, c'est-à-dire des mots restant stables non pas sous l'opération d'image miroir, mais plutôt sous l'action d'un antimorphisme involutif.

D'autre part, certaines suites points fixes sous un opérateur se sont révélées être bien mystérieuses; il suffit de penser au célèbre mot de Kolakoski K=221121221221121122... qui est le point fixe sous l'opérateur de codage par blocs (le mot est égal à ses longueurs de blocs de lettres: ``2'' lettres 2, ``2'' lettres 1, ``1'' lettre 2, ``1'' lettre 1, ...). Plusieurs propriétés combinatoires de ce mot sont encore inconnues: la fréquence des lettres, la récurrence des facteurs, la fermeture de l'ensemble de ses facteurs sous l'image miroir et la complémentation, etc.

Ainsi, avec D. Jamet et G. Richomme, nous nous sommes intéressés à l'étude des points fixes sous l'opérateur de fermeture pseudopalindromique itérative. Dans mon exposé, je vais présenter certains de nos résultats concernant les propriétés combinatoires de ces mots et faisant intervenir entre autres des développements en fractions continues et des morphismes. Je terminerai en proposant certains problèmes ouverts concernant l'algébricité de la ``pente'' de certains de ces points fixes et l'existence d'exposants critiques.

Abstract available as a PDF file.

Thursday 4th December 2008 at 10h Choco (TBA),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 27th November 2008 at 10h15 Damiano Mazza (LIPN, Villetaneuse),
Réécriture, catégories d'ordre supérieur, et expressivité des modèles de calcul concurrent

Abstract: (Hide abstracts)
Un problème fondamental dans la comparaison de différents modèles du parallélisme et de la concurrence est celui de définir la notion de codage, ou de traduction. A ce jour, parmi toutes les notions universellement acceptées de codage entre modèles concurrents, il n'en existe aucune qui s'impose nettement sur les autres. Nous proposons d'étudier la notion de codage en partant de la vision du calcul comme réécriture, et en utilisant des notions venant de la théorie des catégories d'ordre supérieur et de la théorie des structures d'évenemments de Winskel.

Thursday 20th November 2008 at 10h15 Ugo Dal Lago (Bologne),
Taming Modal Impredicativity: Superlazy Reduction

Abstract: (Hide abstracts)
Pure, or type-free, linear lambda calculus is Turing complete once reduction is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing reduction to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, a residual of a box b interacts with the body of another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a (linear) lambda-term finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a lambda-term via superlazy reduction.

Thursday 13th November 2008 at 10h15 Luigi Santocanale (LIF, Marseille),
Outils algébriques pour les logiques modales de point fixe

Abstract: (Hide abstracts)
Dans cet exposé, nous allons d’abord présenter les logiques modales plates de point fixe (flat modal fixpoint logics). Chaque logique de ce type est une extension de la logique modale K et, au même temps, un fragment du $\mu$-calcul modal propositionnel. Nous aborderons le problème de trouver, de façon uniforme, une axiomatisation de ces logiques qui soit complète par rapport à leur interprétation standard sur les modèles de Kripke.

Nous verrons comme certaines idées de l’algèbre, de la coalgèbre, et de la théorie des catégories, sont fondamentales pour notre but: la dualité, par la notion de modalité de couverture, les adjoints, avec la généralisation aux O-adjoints, les objets libres, la notion de point fixe constructif, les rétractés. Ainsi, nous serions en mesure de proposer une axiomatisation complète pour chaque logique plate de point fixe. (Travail en collaboration avec Yde Venema).

Thursday 6th November 2008 at 10h Choco (IML, LAMA),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 23rd October 2008 at 10h15 Christophe Raffalli (LAMA),
PML, où en est-on ?

Abstract: (Hide abstracts)
Je dirai où en est PML, notamment, l'algorithme de typage et le proof-checking. Je montrerai les premiers exemples de programmes prouvés en PML.

Thursday 16th October 2008 at 15h15 Katarzyna Grygiel (Jagiellonian University, Cracovie),
Quantitative approach to lambda calculus

Abstract: (Hide abstracts)
The aim of this talk is to present the problem of enumerating terms in untyped lambda calculus. The very first idea was to compute the asymptotic density of strongly normalizing closed lambda terms among all closed terms of a given size. However, the preliminary task of counting lambda terms turned out to be already non-trivial and challenging and this is therefore as the main theme. I will show recent results which were obtained due to cooperation between universities in Chambery, Versailles and Krakow.

Thursday 16th October 2008 at 10h15 Samuel Mimram (PPS, Paris 7),
Causalité dans les sémantiques interactives

Abstract: (Hide abstracts)
Les sémantiques de jeux ont été introduites pour capturer le comportement interactif des preuves en interprétant les formules par des jeux sur lesquels les preuves induisent des stratégies. L'une des difficultés majeures lors de la définition de telles sémantiques, est de les rendre précises, c'est-à-dire de caractériser les stratégies définissables, qui sont l'interprétation d'une preuve (ou d'un programme par la correspondance de Curry-Howard). L'extension des caractérisations habituelles à des langages de programmation comportant des constructions concurrentes nécessite de repenser en profondeur les définitions habituelles de sémantique des jeux, en menant une analyse fine de la structure dépendances entre les coups dans les stratégies. Nous présentons ici deux approches axiomatiques pour décrire cette structure : l'une externe, fondée sur la présence de certaines tuiles de permutation de coups dans les stratégies, l'autre interne, décrivant la catégorie des stratégies comme une structure algébrique libre.

Thursday 9th October 2008 at 10h Choco (LIX, LIP, IML, PPS),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 2nd October 2008 at 10h15 Michaël Weiss (TCS-Sensor lab, Genève),
Calculabilité des pavages

Abstract: (Hide abstracts)
Au début des années 60, Wang a introduit un modèle de pavage du plan à l'aide de tuiles orientées de taille unitaire aux bords colorées pour résoudre des problèmes de logique. Ce modèle a été montré Turing-équivalent par Berger qui montra qu'un jeu de tuiles pouvait simuler une machine de Turing. Nous nous intéressons a la calculabilité de ce modèle en introduisant des outils sur les pavages permettant d'obtenir des résultats plus généraux sur les jeux de tuiles. A l'aide de notions de simulation, nous obtenons une première approche de l'universalité puis, nous montrons quelques uns des théorèmes fondamentaux de la calculabilité (Kleene, Rice...), dans le cadre des pavages, toujours relativement à certaines notions de simulation. Ces résultats nous permettront d'obtenir dans un premier temps de nouvelles preuves sur des théorèmes classiques des pavages et dans un deuxième temps de construire un cadre de construction de jeux de tuiles apériodiques.

Thursday 25th September 2008 at 10h15 Benoît Masson (LIF, Marseille),
Des piles de sable aux automates de sable

Abstract: (Hide abstracts)

Dans cet exposé, nous commencerons par résumer les résultats connus sur les modèles classiques de piles de sable (SPM, IPM(k)) et sur quelques-unes de leurs extensions. Nous verrons que l'approche combinatoire a des limites, justifiant ainsi leur étude au travers d'un nouveau système dynamique discret, les automates de sable.

Nous définirons ce système, en rappelant en permanence les liens existant entre celui-ci et un autre système dynamique mieux connu, les automates cellulaires. Puis, après avoir rappelé quelques-une des propriétés basiques des automates de sable, nous définirons des propriétés dynamiques à l'aide d'une topologie compacte inspirée de celle utilisée pour l'étude des automates cellulaires.

Ces propriétés permettent une étude plus globale de la dynamique d'un modèle donné, avec des techniques topologiques puissantes. Nous verrons ainsi comment classer les automates selon leur ``chaoticité'', en s'inspirant de la classification pour les automates cellulaires 1D de Kůrka. Ces résultats permettent de souligner que les automates de sable sont un système intermédiaire entre les automates cellulaires de dimension d et d+1.

Thursday 18th September 2008 at 10h15 Pierre Hyvernat (LAMA),
Fonctions booléennes et logique linéaire barycentrique

Abstract: (Hide abstracts)
La logique linéaire s'interprète dans les espaces vectoriels, même si les exponentielles posent problème (on obtient des espaces de dimension infinie). Dans le cas fini, cette interprétation est malheureusement un peu dégénérée car l'interprétation d'une formule (un espace vectoriel) est isomorphe à celle de sa négation (l'espace des formes linéaire sur cet espace). Christine a récemment proposé une solution : en plus de l'espace vectoriel, on rajoute une notion de totalité. Typiquement, une fonction linéaire de A dans B est totale ssi elle envoie les vecteurs totaux sur des vecteurs totaux. Algébriquement parlant, la totalité est un sous-espace affine de l'espace vectoriel considéré.

Christine introduira tout ça avec un peu plus de détails, et expliquera comment obtenir un premier résultat de complétude : complétude d'un calcul booléen basé sur la traduction habituelle du type Bool => Bool dans la logique linéaire. Pierre poursuivra avec un second résultat toujours de complétude : complétude d'une logique linéaire sans exponentielles. (Ça, c'est si la preuve ne « devient » pas fausse d'ici là...)

Le premier résultat ne nécessite aucune connaissance en logique linéaire (si si, c'est vrai), et le second présuppose un modicum de logique linéaire pour comprendre le pourquoi (mais pas le comment). Des connaissances de base en algèbre linéaire sont nécessaires, mais rien de compliqué, et seulement en dimension finie.

Thursday 11th September 2008 at 10h15 Guillaume Theyssier (LAMA),
Automates cellulaires, dynamique topologique et logique

Abstract: (Hide abstracts)
Dans le modèle des automates cellulaires, la non-linéarité est omniprésente. Une voie pour étudier ces objets peut être la théorie du chaos déterministe. Elle a déjà été largement empruntée dans la littérature (avec les travaux de P. Kurka notamment), mais pratiquement toujours en se restreignant à la dimension 1. En ce concentrant sur certaines propriétés autour de la sensibilité aux conditions initiales, nous montrerons dans une première partie de cet exposé que cette restriction n'est pas neutre : une nouvelle classe de comportements dynamiques (les automates cellulaires non sensibles aux conditions initiales mais sans point d'équicontinuité) apparaît à partir de la dimension 2. De la démonstration de l'existence de cette classe, nous tirerons d'autres résultats montrant que la complexité de certaines propriétés fait un bond lorsque l'on quitte la dimension 1.

Dans une seconde partie d'exposé, nous prendrons un peu de recul sur la question de la variation de complexité des propriétés en fonction de la dimension. Nous poserons un cadre logique formalisant ce que l'on peut appeler la ``dynamique topologique'' dans les automates cellulaires. Nous aborderons alors le problème suivant : étant donnée une propriété (une formule dans notre théorie), quel est la complexité de l'ensemble des automates cellulaires qui la satisfont ? cet ensemble est-il arithmétique ? à quelle hauteur dans la hiérarchie ? comment cette hauteur varie avec la dimension ?

Selon la vitalité de l'orateur, le traitement de ce questionnement pour aller du simple traitement d'exemples à la démonstration d'un résultat général.

Thursday 4th September 2008 at 10h15 Tom Hirschowitz (LAMA),
Vers des jeux topologiques

Abstract: (Hide abstracts)
Composition of strategies is the crucial operation of game semantics. It corresponds to cut elimination in proof theory. This paper is an attempt to uncover the sheaf-theoretical nature of these two operations. We define a game semantics with a topological flavor for a variant of Multiplicative Additive Linear Logic (henceforth MALL). We show that the standard notion of strategy leads to a correct, yet incomplete model. We then introduce a new, non-standard notion of ``local'' strategies, which turn out to form a sheaf.

Composition of strategies is generally divided into two steps: interaction, and hiding. In our setting, interaction arises as gluing in the sheaf of local strategies. Hiding along a cut c: U -> V appears here as an instance of a more general operation, ``descent'' along c, which also encompasses cut elimination. Descent along c is a morphism of sheaves on V from the direct image along c of local strategies on U, into cut-free local strategies on V. It arises from a factorisation system, roughly dividing plays into their cut-only and cut-free parts.

Finally, our notion of (winning) local strategy is validated by the expected soundness and completeness results w.r.t. MALL provability.

Monday 1st September 2008 at 14h30 Clément Fumex (LAMA),
Container, dérivation de type et zipper, une répétition de soutenance

Abstract: (Hide abstracts)
Je parlerai des zippers : leurs principes, comment ils amènent à une notion de dérivée de type de données. On verra alors une première définition de cette dérivée par McBride, quelques problèmes et une deuxième définition pour y répondre. Puis nous passerons brièvement aux containers, une notion générale de type de données. Nous verrons comment étendre la notion de dérivée aux containers pour finir sur une formule de Taylor des containers.

Thursday 3rd July 2008 at 10h15 Pierre Hyvernat (LAMA),
Les espaces cohérents et les espaces de finitude

Abstract: (Hide abstracts)
Les espaces cohérents de Jean-Yves Girard et les espaces de finitude de Thomas Ehrhard sont obtenus à partir d'une base « similaire » : l'orthogonalité.

Je commencerais par rappeler comment ça marche (parce que c'est intéressant et pas très compliqué), puis je passerais à une structure mixte qui permet de générer des espaces de finitude « simples » à partir d'espaces cohérents.

Cette construction contient tous les exemples usuels d'espaces de finitude et de plus, elle commute avec les opérations logiques (⅋, ⊗, ⊕, &, ⊸, !, …) Un des aspects intéressants est l'utilisation du théorème de Ramsey infini pour démontrer certaines propriétés de cette construction.

Je finirais par expliquer comment on tombe sur une notion qui généralise les fonctions stable de Berry pour permettre d'interpréter une version simple du λ-calcul algébrique de Lionel, Thomas et consorts.

Remarques : j'essaierais, autant que possible, de ne pas supposer connue toute la logique linéaire. Les deux premiers tiers de mon exposé devraient donc être « self-contained »...

Tuesday 1st July 2008 at 10h30 Laurent Fuchs (Université de Poitiers),
La droite réelle de Harthong-Reeb, un modèle d'une droite réelle constructive ?

Abstract: (Hide abstracts)
La droite réelle de Harthong-Reeb est un modèle non-standard du continu qui est à l'origine de nombreux développements en géométrie discrète (entre autre la droite discrète de Réveillès). Selon Harthong et Reeb eux-mêmes leur modèle n'est pas sans liens avec une approche constructive. Récemment à Poitiers et à La Rochelle nous nous sommes intéressés à cette question en montrant que la droite de Harthong-Reeb vérifie les axiomes de Bridges qui sont une théorie de la droite réelle constructive.

L'orateur propose un deuxième exposé, qui aura peut-être lieu l'après-midi s'il y a des volontaires :

L'algèbre de Grassmann pour définir et manipuler des variétés linéaires discrètes et le plongement géométrique de structures topologiques combinatoires

Résumé :
L'algèbre de Grassmann fournit un langage de représentation des sous- espaces vectoriels d'un espace vectoriel. Ceci permet de manipuler ces sous-espaces sans faire référence directement à un système de coordonnées. Ceci est particulièrement utile lorsque la description ``analytique'' des sous-espaces est compliquée comme, par exemple, pour les variétés linéaires discrètes ou lorsque l'on veut pouvoir représenter la géométrie d'objets subdivisés en toutes dimension comme, par exemple, pour les cartes combinatoires généralisées.

Thursday 26th June 2008 at 10h15 Benoît Montagu (INRIA Rocquencourt),
A Logical Account of Type Generativity: Abstract types have open existential types

Abstract: (Hide abstracts)
We present a variant of the explicitly-typed second-order polymorphic λ-calculus with primitive open existential types, i.e., a collection of more atomic constructs for introduction and elimination of existential types. We equip the language with a call-by-value small-step reduction semantics that enjoys the subject reduction property. We claim that open existential types model abstract types and module type generativity. Our proposal can be understood as a logically-motivated variant of Dreyer’s RTG where type generativity is no more seen as a side effect. As recursive types arise naturally with open existential types, even without recursion at the term-level, we present a technique to disable them by enriching the structure of environments with dependencies. The double vision problem is addressed and solved with the use of additional equalities to reconcile the two views.

Thursday 19th June 2008 at 10h Choco (Southampton, Copenhague, et PPS),
Séminaire Choco: bigraphes

Abstract: (Hide abstracts)
Voir la page dédiée.

Tuesday 10th June 2008 at 10h15 Alexandre Miquel (PPS, Paris 7),

Abstract: (Hide abstracts)
Cours puis groupe de travail sur la réalisabilité avec Alexandre Miquel. Détails ici.

Thursday 29th May 2008 at 10h15 Fairouz Kamareddine (Université Heriot-Watt, Edimbourg),
Une computerisation graduelle des textes mathematiques dans le systeme MathLang

Abstract: (Hide abstracts)
Le project MathLang a pour but de computeriser des textes de mathematiques selon des degres de formalisation differents, et sans preciser d'avance un engagement dans:
* un logique particulier (par example, sans devoir choisir comme base une theorie des ensembles, une theorie des categories, une theorie des types, etc.)
* un systeme de demonstration particulier (par example, sans devoir choisir comme systeme de demonstration Mizar, Isaeblle, Coq, PML, etc.).

MathLang laisse les choix concernant les systemes de demonstration et de la logique ouverts tant que c'est possible. En plus, MathLang permet des niveaux varies de computerisation, et n'insiste pas qu'une formalisation soit complete comme c'est fait dans les fondations de la mathematiques a la Russell et Frege ou dans les systemes de demonstration (comme initie par de Bruijn). Pendant la computerisation, le text mathematique est d'abord insere dans l'ordinateur tel qu'il est ecrit par le mathematicien sur papier. Puis un ou plusieures aspets de MathLang sont appliques au texte pour donner des versions du texte qui sont (automatiquement) controles a des niveaux differents:
1. Un aspect de base est l'extension du texte avec l'information categorique (terme, nom, adjectif, proposition, etc) ou la coherence et la structure grammaticale du texte sont controlees automatiquement.
2. Un autre aspect partage le texte en parties annotees par des relations (e.g., Corollaire A utilise Theorem B) et automatiquement controle la structure logique du texte (ce n'est la correction logique du texte).
3. Un autre aspect transforme le texte alors que les trous dans les preuves sont evidents.
4. D'autres aspects transforment cette version derniere en une formalisation complete (dans Coq, Mizar, Isabelle, etc).

MathLang a ete cree par Fairouz Kamareddine et J.B. Wells en 2000. Nous avons computeriser des textes dans MathLang (pas a pas) jusqu'a des formalisations completes dans Coq et Mizar (aussi Isar/Isabelle). Depuis 2002, 4 etudiants de theses (Manuel Maarek, Kryztof Retel, Robert Lamar et Christoph Zengler) et des dizaines d'etudiants de master et de BSc ont contribue au design et a l'implantation de MathLang et a son utilisation pour la computerisation des textes de Maths.

S'il reste du temps, Fairouz pourra enchaîner sur un exposé plus orienté lambda-calcul:

Titre: Parametres dans le lambda calcul type.

Les fonctions dans le lambda calcul sont toujours d'ordre superieur. Traditionellement, les fonctions en maths sont d'ordre inferieur. Ici, on donne le lambda calcul avec des fonctions d'ordre inferieur et on divise le cube de Barendregt en 8 sous-cubes qui permettent des meilleures representations des constructeurs dans les languages ML, LF et Automath.

C'est un travail commun avec Twan Laan et Rob Nederpelt.

Thursday 22nd May 2008 at 10h15 Emmanuel Jeandel (LIF, Marseille),
Les pavages comme outils de la logique

Abstract: (Hide abstracts)
La théorie des pavages par tuiles de Wang a été inventée par (surprise) Hao Wang afin de proposer un problème combinatoire concret correspondant au pouvoir d'expressivité d'un fragment de la logique du premier ordre. La théorie des pavages s'est en fait révélée comme une théorie élégante s'exprimant facilement logiquement, et a ainsi apporté de nombreux résultats en logique mathématique.
Il s'agit dans cet exposé de proposer une présentation des liens entre pavages et logique. On analysera en particulier comment deux des théorèmes fondamentaux sur les pavages se traduisent :
- Par l'existence d'une théorie complète finiment axiomatisable et superstable [Makowsky, Poizat]
- Par le fait que le fragment AEA de la logique du premier ordre forme une classe de réduction conservative [Büchi, Kahr-Moore-Wang]
tout en expliquant bien entendu ce que signifient les nombreux mots potentiellement obscurs des phrases précédentes.
Aucune connaissance sur les pavages n'est nécessaire. Une connaissance rudimentaire de la logique du premier ordre sera appréciée.

Thursday 15th May 2008 at 10h15 Sylvain Lebresne (PPS, Paris 7 et Logical, LIX),
Un système d'exceptions pour le Système F

Abstract: (Hide abstracts)
Les exceptions sont généralement vues comme un mécanisme modifiant le flot de contrôle d'un programme. Cette vision cantonne les exceptions aux langages pour lesquels la notion de flot de contrôle est bien définie, ce qui n'est généralement pas le cas pour les langages de la théorie des types. Nous présenterons un mécanisme où les exceptions sont attachées aux valeurs plutôt qu'au flot de contrôle, ainsi qu'un système de types pour ces exceptions basé sur la notion de corruption. Nous montrerons que cette notion, utilisée à travers une relation de sous-typage, permet la détection statique d'exceptions non rattrapées, et ce sans compromettre la propagation automatique des exceptions. Nous illustrerons ce système d'exceptions dans le cadre d'une extension du Système F, utilisé ici comme une première étape vers des systèmes de types plus riches (avec pour horizon le calcul des constructions). Enfin, nous présenterons un modèle de réalisabilité pour justifier et expliquer la notion de corruption dans notre calcul.

Thursday 24th April 2008 at 10h Projet Choco (PPS et Cambridge),
Quatrième journée Choco

Abstract: (Hide abstracts)
Cf le site idoine:

Thursday 17th April 2008 at 10h Samuel Thibault (XenSource),
Petite histoire des threads migrateurs et de l'algorithmie des bulles, ou comment les ambients sauvent la banquise

Abstract: (Hide abstracts)
Comme le montrent les publicités dans les magazines (multi-coeur par-ci, hyperthread par-là), la tendance des architectures des ordinateurs est à la parallélisation, et l'on commence donc dans le grand public à parler de programmation avec des threads. Du côté des machines de calcul scientifique, on mélange en fait allègrement ces technologies de manière hiérarchique pour aboutir à de véritables cathédrales, sur lesquelles on exécute une armée de threads. Cependant, pour obtenir une exécution _efficace_ (et donc économiser du temps, des machines ou de l'énergie), il est indispensable de distribuer de manière raisonnée ces threads sur ces machines. La tâche est d'autant plus ardue que les threads peuvent en créer d'autres, éventuellement de manière irrégulière. Durant ma thèse, j'ai proposé la notion de /bulles/, qui regroupent de manière récursive les threads et apportent ainsi une certaine structure aux applications de calcul scientifique. En modélisant par ailleurs les machines de calcul sous forme d'un arbre, on ramène ainsi notre problème à la mobilité des bulles et threads sur cet arbre. Une boîte à outil permet alors d'implémenter des algorithmes de placement/redistribution pour les appliquer à des applications bien concrètes. On peut alors observer des gains de performances de l'ordre de 20 à 40% par rapport à un ordonnancement classique ! Je débuterai mon exposé en expliquant quelques détails architecturaux importants par rapport à l'efficacité de l'exécution des threads d'une application. J'introduirai alors ce que j'entends par ``ordonnancement'', ``placement'' et ``migration'' des threads et bulles. Je présenterai ensuite la boîte à outils au travers de quelques exemples, et l'on pourra discuter notamment de la ressemblance intriguante avec des ambients.

Thursday 10th April 2008 at 10h15 Robert Bonnet (LAMA),
Algèbre libre sur un monoïde et demi-treillis compacts

Abstract: (Hide abstracts)
Cet exposé, est une partie d’un article en cours, en collaboration avec {\it Latifa Faouzi} (Fes et Casablanca) et se compose de deux parties indépendantes.
PARTIE I: $k$-algèbre libre sur un monoïde.
On considère un corps commutatif $k$ et un monoïde (= demi-groupe commutatif et unitaire) $M$. On désigne par $k[M]$ la $k$-algèbre sur le monoïde $M$, i.e. l’espace vectoriel sur $k$ ayant $M$ comme base, c’est alors aussi un anneau puisque $M$ est stable par produit. L’exemple type étant l’algèbre des polynômes sur $k$. Le corps $k$ étant fixé, on montre plusieurs propriétés de la classe des algèbres sur un monoïde. Par exemple $k[X] x k[Y]$ est une $k$-algèbre libre sur un monoïde. On développe aussi une classe plus large où le produit de deux élements de $M$ est soit $0$, soit un élement de $M$.
PARTIE II: Demi-treillis compact. Dans cette partie, les monoïdes ne sont pas unitaires. On considère un triplet $(L,O,.)$ où $(L,O)$ est un espace compact séparé, $(L,.)$ est un monoïde idempotent (mais sans unité). On suppose que l’application $(x,y) -> x. y$ est continue. En interprétant $x . y$ comme l’infimum de $x$ et de $y$, $(L,.)$ est un (inf-)demi-treillis et $.$ est continue. Noter que $L$ est alors un ensemble ordonné en posant $x \leq y$ ssi $x . y = x$. On montre quelques propriété de cette classe de structures. Par exemple, une telle structure possède un plus petit élément $0$ et toute partie non vide et filtrante supérieurement possède un supremum. La topologie est alors déterminée par l’ordre: une sous-base de la topologie est formée d’élements de la forme $U_x := \{ y \in L : y \geq x \}$ et $L \setminus U_x$ où $x$ est un élément “compact” de $L$. Ces notions de demi-treillis compacts apparaissent lors de l’étude des domaines et des treillis algébriques.
PARTIE III: Le lien. Si on considère le corps $k = \{0,1\}$ ayant deux éléments et le monoïde $M$ idempotent, alors $k[M]$ est une algèbre de Boole, dont l’espace des ultrafiltres (ou des idéaux maximaux) est un demi-treillis compact et “réciproquement”.
[1] Bourbaki N.: Eléments de mathématiques, Algèbre, Chapitres 1--3, Hermann, 1970.
[2] Lang S.: Algebra, Addision-Wiesley Pub, 1970.
[3] Gierz, G., Hofmann K. H., Keimel K., Lawson J. D., Mislove M. and Scott D. S.: Continuous lattices and domains, Encyclopedia of Mathematics and its Applications, 93. Cambridge University Press, Cambridge, 2003, 591 pp.

Tuesday 8th April 2008 at 10h30 Mouhammad Said (LAMA),
Géométrie multi-résolution des objets bruités

Abstract: (Hide abstracts)
L'objectif de cet exposé est de présenter le contexte et les motivations ayant conduit à mon sujet de thèse : Géométrie multirésolution des objets discrets bruités. On commencera par présenter quelques outils classiques autour des droites discrètes et leurs applications à l'estimation de quantités géométriques sur des formes discrètes. L'extension de ces outils aux formes discrètes bruitées sera ensuite abordée. On en déduira les quelques axes de recherche qui seront explorés dans ma thèse.

Thursday 3rd April 2008 at 10h15 Laurent Vuillon (LAMA),
Combinatoire des mots et conjecture de Fraenkel

Abstract: (Hide abstracts)
Ce séminaire donnera les liens entre un problème de recouvrement des entiers et la combinatoire des mots afin d'étudier la conjecture de Fraenkel. Cette conjecture a été formulée dans le cadre de la théorie des nombres il y a maintenant plus de 30 ans. Elle prétend que pour k > 2 entier fixé, il y a une unique façon de recouvrir les entiers par $k$ suites de Beatty avec des fréquences deux à deux distinctes. Ce problème peut être exprimé en termes de combinatoire des mots de la façon suivante: pour un alphabet à k lettres, il existe une unique suite équilibrée avec des fréquences de lettres deux à deux distinctes qui est exactement la suite de Fraenkel notée $(F r_k )^{omega}$ où F r_k = F r_{k-1} k F r_{k-1}, avec F r_3 = 1213121. Cette conjecture est prouvée pour k = 3, 4, 5, 6 d'après les travaux de Altman, Gaujal, Hordijk et Tijdeman ainsi que dans d'autres cas particuliers. Dans ce séminaire, nous présenterons donc une synthèse sur ce sujet et la résolution de la conjecture dans un cas particulier.

Tuesday 1st April 2008 at 10h30 Karim Nour (LAMA),

Abstract: (Hide abstracts)

Thursday 27th March 2008 at 10h15 Pierre Guillon (Univ. Marne-la-Vallée),
Automates cellulaires: trace et nilpotence

Abstract: (Hide abstracts)
Un automate cellulaire est un modèle de calcul parallèle synchrone, qui consiste en une juxtaposition d'automates d'état fini (cellules) dont l'état évolue dans le temps en fonction de celui de leurs voisins. Malgré la simplicité de cette règle locale, des comportements très variés peuvent être observés dans l'évolution d'une population de cellules.
Nous présentons ici quelques notions topologiques décrivant ces dynamiques. Nous nous intéressons en particulier à la nilpotence, qui correspond à un comportement ultimement stable. Nous en donnons une caractérisation utilisant la trace, qui est le mot infini représentant la suite des états pris par une cellule donnée.

Thursday 20th March 2008 at 10h Projet Choco (TBA),
Quatrième journée Choco

Abstract: (Hide abstracts)
Voir la page web idoine.

Thursday 13th March 2008 at 10h15 Lionel Vaux (IML),
λ-calcul algébrique

Abstract: (Hide abstracts)
On propose une extension naturelle du λ-calcul autorisant la formation de combinaisons linéaires de termes. Ceci reflète dans la syntaxe la sémantique quantitative du λ-calcul simplement typé dans les espaces de finitude, où les types sont interprétés par des espaces vectoriels particuliers, et les λ-termes par des fonctions entre ces espaces.
On étudie les effets de la présence de coefficients scalaires sur la réduction: après avoir étendu la β-réduction en une relation contextuelle et confluente, on s'intéresse à la cohérence du calcul et à des propriétés de normalisation dans un cadre typé.
On établit enfin une correspondance entre ce λ-calcul algébrique et le λ-calcul linéaire-algébrique d'Arrighi et Dowek en montrant qu'ils correspondent à deux stratégies de réduction (par nom et par valeur) d'une syntaxe commune.

Thursday 6th March 2008 at 10h15 Muhammad Humayoun (LAMA),
Software Specifications and Mathematical Proofs in Natural Languages

Abstract: (Hide abstracts)
Software specifications, Software/Hardware standards like RFCs, patents etc and Mathematical proofs are normally written in plain natural language. Natural languages are rich, complex, and ambiguous. Having this in mind, Formal methods try to solve this problem by replacing natural languages with rich mathematical formalisms which are understood by model checkers or theorem provers. They are very precise, accurate and clear but not easily understood by domain experts such as Software designers, programmers, engineers and Mathematicians.
This project is an attempt to make a connection between formal and natural languages. We are developing a controlled natural language having large coverage, which will be good enough for writing Software Specifications and Mathematical Proofs interactively.
We are currently working on parsing and translation of Mathematical proofs written in Natural language (English). Therefore I'll talk on Mathematical proofs for most of the time. Specifically I'll explain the implementation details.
Project homepage: .

Friday 22nd February 2008 at 14h Damien Pous (Plume),
Soutenance de thèse

Abstract: (Hide abstracts)

Thursday 21st February 2008 at 10h Projet Choco (Bologne, INRIA Sophia et IML),
Troisième journée Choco

Abstract: (Hide abstracts)

Thursday 14th February 2008 at 10h15 Giulio Manzonetto (PPS (Paris 7)),
Modèles effectifs du lambda calcul

Abstract: (Hide abstracts)
On étudie la question de l’existence d’un modèle non-syntaxique du lambda calcul appartenant aux sémantiques principales et ayant une théorie équationnelle ou inéquationnelle r.e. (récursivement énumérable).
Cette question est une généralisation naturelle du problème de Honsell et Ronchi Della Rocca (ouvert depuis plus que vingt ans) concernant l’existence d’un modèle continu de lambda-beta ou lambda-beta-eta. On introduit une notion adéquate de modèles effectifs du lambda-calcul, qui couvre en particulier tous les modèles qui ont été introduits individuellement en littérature, et on prouve que la théorie inéquationnelle d’un modèle effectif n’est jamais r.e.; en conséquence sa théorie équationnelle ne peut pas être lambda-beta ou lambda-beta-eta.
On montre aussi que la théorie équationnelle d’un modèle effectif vivant dans la sémantique stable ou fortement stable n’est jamais r.e. En ce qui concerne la sémantique continue de Scott, on démontre que la théorie inéquationnelle d’un modèle de graphe n’est jamais r.e. et qu’il existe beaucoup de modèles de graphes effectifs qui ont une théorie équationnelle qui n’est pas r.e.

Thursday 7th February 2008 at 10h15 Srecko Brlek (LaCIM, UQAM),
Ensembles discrets ronds

Abstract: (Hide abstracts)
We analyze the moment of inertia $\MI(S)$, relative to the center of gravity, of finite plane lattice sets $S$. We classify these sets according to their roundness: a set $S$ is rounder than a set $T$ if $\MI(S) < \MI(T)$. We show that roundest sets of a given size are strongly convex in the discrete sense. Moreover, we introduce the notion of quasi-discs and show that roundest sets are quasi-discs. We use weakly unimodal partitions and an inequality for the radius to make a table of roundest discrete sets up to size $40$. Surprisingly, it turns out that the radius of the smallest disc containing a roundest discrete set $S$ is not necessarily the radius of $S$ as a quasi-disc.

Thursday 31st January 2008 at 10h Projet Choco (PPS et IML),
Deuxième journée Choco

Abstract: (Hide abstracts)
Deuxième édition du séminaire Choco.
Le programme prévu est le suivant:
10h - 12h Damiano Mazza (PPS, Paris), Objets d'interaction et réseaux différentiels
14h - 15h30 Michele Pagani (PPS, Paris), Between interaction and semantics: visible acyclic nets
16h - 17h30 Lionel Vaux (IML, Marseille), Produit de convolution et composition parallèle

Thursday 24th January 2008 at 10h15 Tom Hirschowitz (LAMA),
Une théorie des théories des jeux

Abstract: (Hide abstracts)
(En collaboration avec André et Michel Hirschowitz.)
La sémantique des jeux a fait ses preuves comme source de modèles pleinement abstraits pour langages de programmation ou théories de la démonstration. De tels modèles apparaissent comme catégories de jeux et stratégies, mais on en compte de nombreuses variantes, qu'on ne sait pas bien relier entre elles. D'où la question: qu'est-ce qu'une catégorie de jeux et stratégies?
On donne une définition catégorique générale de jeu, en décrivant la catégorie de stratégies associée. On définit ensuite une construction catégorique générant un jeu à partir de données plus élémentaires. On montre comment les jeux de Hyland et Ong avec switching entrent dans ce cadre.

Thursday 17th January 2008 at 10h15 Francesco Zappa-Nardelli (Moscova (INRIA)),
Oracle Semantics for Concurrent Separation Logic

Abstract: (Hide abstracts)
We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor---a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow constructs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics. Using our modularity principle, we proved the sequential CSL rules (those that are inherited from sequential Separation Logic) simply by adapting Appel & Blazy's machine-checked sequential-separation-logic soundness proofs with minimal changes. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimizing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent setting. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine. (Joint work with Aquinas Hobor and Andrew Appel (Princeton University)).

Wednesday 16th January 2008 at 14h Stéphane Le Roux (Mathematical Components (INRIA-Microsoft Research)),
Soutenance de thèse

Abstract: (Hide abstracts)

Thursday 10th January 2008 at 10h15 Frédéric Ruyer (LAMA),
Modèles pour le calcul et la logique

Abstract: (Hide abstracts)
Nous présentons une classe de modèles du lambda-calcul et de la logique du second ordre. Les modèles sont basés sur des treillis et interprètent la réduction, ainsi que la relation de réalisabilité, à l'aide de la relation d'ordre. Nous tenterons de dégager les liens avec les algèbres de Heyting et les modèles à base de cpo du lambda-calcul.

Friday 21st December 2007 at 10h Dragisa Zunic (ENS Lyon),
Soutenance de thèse

Abstract: (Hide abstracts)

Thursday 20th December 2007 at 10h Projet Choco (ANR),
Journée interne projet Choco

Abstract: (Hide abstracts)
10h - 12h Samuel Mimram (PPS, Paris 7), Sémantiques de jeux asynchrones
14h - 15h30 Marc de Falco (IML, Marseille), Géometrie de l'interaction des réseaux différentiels et application à l'étude des π-termes
15h30 - 17h Auélien Pardon (LIP, ENS Lyon), Une approche algébrique et modulaire de la syntaxe avec lieurs

Abstract available as a PDF file.

Thursday 13th December 2007 at 10h15 Stefano Berardi (Turin),
A computational interpretation of classical proofs through parallel computations

Abstract: (Hide abstracts)
We argue in favor of the following thesis: there is an intric link between the computation we can unwing from classical proofs and parallel computations. We introduce a model for computations extracted from classical proofs based on parallel computations and on the concept of learning in the limit. The aim of our research is designing parallel extensions of the existing continuation languages.

Wednesday 12th December 2007 at 14h Peter Battyanyi (LAMA),
Normalization properties of symmetric logical calculi

Abstract: (Hide abstracts)
Dans les années quatre-vingt-dix, on a remarqué ce que l'isomorphisme de Curry-Howard peut être étendu à la logique classique. De nombreux calculs ont été développés pour constituer la base de cette extension. On étudie dans cette thèse quelques uns de ces calculs.
On étudie tout d’abord le lambda-mu-calcul simplement typé de Parigot. Parigot a prouvé par des méthodes sémantiques que son calcul est fortement normalisable. Ensuite, David et Nour ont donné une preuve arithmétique de la normalisation forte de ce calcul avec la règle mu' (règle duale de mu). Cependant, si l'on ajoute au lambda-mu-mu'-calcul la règle de simplification rho, la normalisation forte est perdue. On monte que le mu-mu'-rho-calcul non-typé est faiblement normalisable et que le lambda-mu-mu'-rho-calcul typé est aussi faiblement normalisable. De plus, on examine les effets d'ajouter quelques autres règles de simplification. On établit ensuite une borne de la longueur des séquences de réduction en lambda-mu-rho-theta-calcul simplement typé. Ce résultat est une extension de celui de Xi pour le lambda-calcul simplement typé. Enfin, on présente une preuve arithmétique de la normalisation forte du lambda-calcul symétrique de Berardi et Barbanera.

Wednesday 12th December 2007 at 10h Ralph Matthes (CNRS, IRIT),
Substitution - des solutions surprenantes avec des familles inductives

Abstract: (Hide abstracts)
Des familles inductives de types de données servent bien à représenter le lambda-calcul: le paramètre de la famille décrit l'ensemble de noms de variables libres admises, et le changement du paramètre au cours de la récurrence reflète la génération de noms pour les variables liées. Cette représentation satisfait les propriétés de base de la substitution, dictées par la théorie des catégories. C'est bien connu.
On veut aller plus loin: On encapsule des sous-expressions de lambda-termes comme si elles n'étaient que des noms de variables libres. Ceci donne le lambda-calcul avec aplatissement explicite (une forme de substitution explicite). Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont offertes par aucun assistant de preuves, or elles pouvaient être encodées dans Coq. Là, déjà la notion d'une occurrence libre d'une variable est un défi pour la conception mathématique.
Heureusement, la vérification entière se fait dans Coq, le plus grand problème étant un affaiblissement de la règle que la substitution qui remplace chaque variable par le terme qui consiste de cette variable n'a aucun effet. En plus, toute notre théorie axiomatique est justifiée dans le calcul des constructions inductives avec insignifiance des preuves.

Thursday 6th December 2007 at 10h15 Jacques-Olivier Lachaud (LAMA),
Estimation robuste de courbure

Abstract: (Hide abstracts)
We introduce a new curvature estimator based on global optimisation. This method called Global Min-Curvature exploits the geometric properties of digital contours by using local bounds on tangent directions defined by the maximal digital straight segments. The estimator is adapted to noisy contours by replacing maximal segments with maximal blurred digital straight segments. Experimentations on perfect and damaged digital contours are performed and in both cases, comparisons with other existing methods are presented.

Thursday 22nd November 2007 at 10h15 Francesco Zappa-Nardelli -- Annulé (INRIA Rocquencourt),
Oracle Semantics for Concurrent Separation Logic

Abstract: (Hide abstracts)
We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor---a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow constructs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics. Using our modularity principle, we proved the sequential CSL rules (those that are inherited from sequential Separation Logic) simply by adapting Appel & Blazy's machine-checked sequential-separation-logic soundness proofs with minimal changes. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimizing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent setting. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine.

Thursday 15th November 2007 at 10h15 Thomas Fernique (LIRMM),
Reconnaissance de plan et fractions continues

Abstract: (Hide abstracts)
Une manière de stocker de manière économe un gros objet géométrique discret (images 3D acquises expérimentalement etc.) est de le vectoriser. Une façon de procéder est de le décomposer en plans discrets (approximations de plans euclidiens). Pour cela, un problème crucial est celui de la reconnaissance de plan : déterminer si un ensemble discret est ou non inclus dans un plan discret. Nous présentons une approche originale, qui généralise une approche similaire pour le cas de la reconnaissance de droites. Plus précisément, on montre comment calculer un développement en fraction continues multi-dimensionnel du vecteur normal d'un plan discret simplement en lisant les configurations locales de ce plan. Ce procédé peut alors être étendu à des ensembles discrets plus généraux, bien qu'ils n'aient pas forcément de vecteur normal. Les développements de plans possèdent cependant des propriétés qui permettent finalement de les reconnaître.

Thursday 8th November 2007 at 11h Alexandre Miquel (PPS, Paris 7),
L'effectivité expérimentale de la preuve mathématique

Abstract: (Hide abstracts)
La correspondance de Curry-Howard permet d'interpréter chaque démonstration mathématique comme un programme réalisant une certaine spécification (déduite de la formule démontrée). Mais que se passe-t-il quand la démonstration fait appel à des hypothèses expérimentales - par exemple des lois de la physique?

Dans cet exposé, je me propose d'étudier la frontière entre le raisonnement mathématique et les hypothèses empiriques sur lesquelles reposent les sciences expérimentales. Pour cela, je partirai d'un problème soulevé par le philosophe et épistémologue Karl R. Popper lié à l'utilisation des formalismes mathématiques les plus abstraits dans un cadre empirique. Je montrerai alors comment les techniques modernes de réalisabilité permettent de résoudre ce problème, et suggèrent ainsi des pistes inédites pour combiner de manière effective le raisonnement mathématique avec les protocoles expérimentaux.

Thursday 25th October 2007 at 10h30 Richard Garner (Uppsala),
Categorical models of dependent type theory

Abstract: (Hide abstracts)
A gentle introduction to categorical models of dependent type theory. As a warm up, Richard will explain the interpretation in locally cartesian closed categories (LCCCs), and why it necessarily leads to extensional models of type theory. Then, he will, rather informally, try to explain why models of intensional type theory should look like weak omega categories (read the ordinal ``omega'').

Friday 19th October 2007 at 10h30 Jules Villard (LSV (ENS Cachan)),
Une logique spatiale pour le pi-calcul appliqué

Abstract: (Hide abstracts)
La complexité de l'étude formelle des protocoles cryptographique se situe à plusieurs niveaux. Il faut d'abord modéliser les communications qui ont lieu entre les participants, puis définir précisément les propriétés que l'on souhaite vérifier. Celles-ci peuvent être assez simples à exprimer, comme les propriétés de secret, ou très complexes, comme les propriétés de résistance à la coercition dans les protocoles de vote. Le pi-calcul appliqué est de plus en plus utilisé pour formaliser des protocoles cryptographiques. Il étend le pi-calcul traditionnel en permettant aux processus de manipuler aisément des termes dotés d'une théorie équationnelle. On peut par exemple y inclure des primitives pour le chiffrement ou la signature de message, la création de paires de clés privées/publiques, ou toute autre fonction utile pour le protocole à formaliser. Différentes équivalences permettent ensuite de comparer les processus, dont l'équivalence statique qui, intuitivement, exprime ce qu'un attaquant peut déduire d'un protocole à une étape donnée de son exécution. Pour écrire les propriétés à vérifier sur ces protocoles, on a usuellement recours à différentes logiques, telles que les logiques de Hennessy Milner, de Cardelli-Gordon, et de Caires. L'une de ces logiques est la logique spatiale, qui permet de décrire non seulement les communications dont est capable un processus, mais aussi leur localisation au sein de celui-ci. Ceci permet par exemple de distinguer les différents participants d'un protocole. Cette logique apparaît donc comme un point de départ pertinent pour l'étude de protocoles cryptographique. Le but de ce travail était d'adapter la logique spatiale au traitement du pi-calcul appliqué et d'étudier son expressivité, notamment en termes de propriétés de secrets, sécurité, déductibilité, etc. Nous introduirons tout d'abord la logique spatiale du pi-calcul appliqué que nous avons définie, avant de présenter les résultats théoriques d'expressivité obtenus dans ce nouveau cadre (intensionalité, élimination des quantificateurs, ...), qui rejoignent ceux déjà connus pour le pi-calcul. Enfin, nous donnerons quelques intuitions concernant les propriétés de sécurité et de secret qu'il est possible d'exprimer au sein de la logique, notamment en donnant des formules qui caractérisent l'équivalence statique.

Thursday 18th October 2007 at 10h15 Nicolas Ollinger (LIF),
Pavages: de l'apériodicité à l'indécidabilité

Abstract: (Hide abstracts)
Dans cet exposé, nous démontrerons le résultat d'indécidabilité obtenu par R. Berger en 1964 sur les pavages : savoir, étant donné un jeu fini de tuiles de Wang, s'il existe un pavage valide du plan par ces tuiles est indécidable. Après une brève discussion sur différentes façons de définir des jeux de tuiles et les pavages du plan engendrés, nous nous intéresserons à la problématique de l'apériodicité, introduite par H. Wang. Dans l'esprit des constructions originelles de R. Berger et R. M. Robinson, nous construirons un jeu de tuiles apériodique et nous montrerons comment ce jeu de tuiles peut être étendu pour générer les pavages limites de n'importe quelle substitution 2x2. Fort de cette construction, nous pourrons calculer dans les pavages et obtenir les résultats d'indécidabilité annoncés.

Abstract available as a PDF file.

Monday 15th October 2007 at 10h Muhammad Humayoun (LAMA),
Certified software specifications and Mathematical Proofs in Natural Languages

Abstract: (Hide abstracts)
In this talk, I will present our work in which we are trying to make a connection between formal and natural languages. We aim to develop tools and resources capable of translating between natural languages and formal languages. I will present our attempts in translating mathematical proofs written in natural language into formal proofs. The implementation of our work is based on the Grammatical Framework (GF). GF is a grammar formalism based on type theory, which provides a special purpose language for defining grammars, and a compiler for this language. Further I will give an overview of the future work i.e. Checking formal software specifications with the specifications written in a natural language and to validate whether they correspond to each other or not. I will also argue that it is a very hard problem to generate a good quality text from a formalism. A natural motivation for this work is the fact that it is a normal practice in industry to write specifications in natural language. In a similar way, all the standards such as RFCs, ISO, ANSI, patents are written in plain natural language. Therefore this resource has an immediate usability in the industry. It will help to overcome the difficulties that prevent software designers & engineers to use formal methods. This Project has its usefulness in formal methods, Human computer interaction, natural language technology and Mathematical teaching.

Thursday 11th October 2007 at 10h15 Giovanni Feverati (Laboratoire d'Annecy-le-Vieux de Physique Théorique),
An evolutionary model with Turing machines

Abstract: (Hide abstracts)
Inspired by the unanswered question: why eukariotic DNA has a so large non-coding fraction, we try computer simulations with an evolutionary toy model based on Turing machines. This lead us to describe how the fitness of an ``organism'' and the evolution rate relate to the coding/non-coding ratio. The evolutionary advantage of having a large reservoir of non-coding states is emphasised.

Friday 5th October 2007 at 10h15 Assia Mahboubi (INRIA/ Microsoft Research),
Réflexions sur les preuves formelles en Coq

Abstract: (Hide abstracts)
En 2004, G. Gonthier a achevé la preuve formelle du théorèmes de quatre couleurs dans l'assistant à la preuve Coq. L'une des clefs de cette réussite est une utilisation intensive de techniques dites de ``réflexion à petite échelle'', soutenues par une extension du langage de tactiques de Coq. Cette extension, ainsi qu'une partie des bibliothèques développées pour la preuve, sont actuellement utilisées comme point de départ pour le projet de formalisation d'une somme substantielle de théorie des groupes finis, dans l'équipe Composants Mathématiques du centre commun INRIA MSR. Il s'agit cette fois de construire une preuve formelle du théorème de Feit-Thompson (1963), qui constitue un passage a l'échelle significatif pour les contributions issues de la preuve du théorèmes des quatre couleurs. Le but de cette expérience est de comprendre comment mener à bien le développement de bibliothèques de mathématiques formalisées, réutilisables et combinables. Nous tenterons d'abord de dégager les difficultés que présente la réalisation de telles bibliothèques, puis de présenter les solutions qui se dégagent de la preuve du théorème des quatre couleurs, et en particulier le langage de tactiques ssreflect. Enfin, si le temps le permet, nous présenterons brièvement les nouvelles questions soulevées par la formalisation de théorie des groupes finis, ainsi que l'état actuel de cette construction.

Thursday 27th September 2007 at 10h15 Pierre Hyvernat groupe de lecture (LAMA),
Une question de Pierre + Curry-Howard et les protocoles

Abstract: (Hide abstracts)
Pierre Hyvernat (LAMA) prendra environ 1/2h pour poser une question sur laquelle il bute actuellement. Ensuite, séance lecture sur le papier de Krivine et Legrandgérard, téléchargeable ici: krivine/articles/Network.pdf.

Résumé du papier: On décrit une relation remarquable entre la notion de formule valide du calcul des prédicats et la spécification de protocoles réseau. On donne des exemples comme l'acquittement d'un ou plusieurs paquets.

Thursday 20th September 2007 at 10h15 Frédéric Prost (LIG (équipe CAPP)),
Traitement de la non-compositionalité dans un langage de programmation fonctionel quantique

Abstract: (Hide abstracts)
Nous proposons une extension du lambda-calcul traditionel dans lequel les termes sont utilisés pour manipuler un artefact de calcul externe (bits quantiques, brins d'ADN etc.). Nous introduisons deux nouveaux lieurs de noms : $nu$ et $rho$. $new x.M$ dénote un terme dans lequel $x$ est une référence abstraite, alors que dans $rho y.M$, $y$ est une référence conrète. Nous montrons les différences de ces deux lieurs par rapport au $lambda$ en termes d'$alpha$ équivalence, d'extrusion, de garbage collection etc. Nous illustrons l'intérêt de ces nouveaux lieurs en développant un langage de programmation quantique typé dans lequel la duplication de qbits abstrait est permise alors que la duplication de qbits concrets est interdite. Cela permet un langage plus expressif que ceux proposés dans la littérature actuelle.

Thursday 12th July 2007 at 11h30 Humayoun Muhammad
Urdu Morphology, Orthography and Lexicon Extraction

Abstract: (Hide abstracts)
Urdu is a challenging language because of, first, its Perso-Arabic script and second, its morphological system having inherent grammatical forms and vocabulary of Arabic, Persian and the native languages of South Asia. This paper describes an implementation of the Urdu language as a software API, and we deal with orthography, morphology and the extraction of the lexicon. The morphology is implemented in a toolkit called Functional Morphology, which is based on the idea of dealing grammars as software libraries. Therefore this implementation could be reused in applications such as intelligent search of keywords, language training and infrastructure for syntax. We also present an implementation of a small part of Urdu syntax to demonstrate this re-usability.

Thursday 12th July 2007 at 10h15 Jean Quilbeuf
Elimination des coupures en déduction naturelle propositionnelle intuitionniste avec disjonction.

Abstract: (Hide abstracts)
Je présente la preuve de Prawitz de la faible normalisation de l'élimination des coupures en déduction naturelle propositionnelle intuitionniste avec disjonction. On déduit ensuite la propriété de la sous-formule et la décidabilité de ce système. Il s'agit du travail fait lors de mon stage M1.

Friday 6th July 2007 at 15h Thomas Ehrhard
Traduction d'un pi-calcul finitaire et polyadique dans les réseaux d'interaction différentiels

Abstract: (Hide abstracts)
On présentera (il s'agit d'un travail commun avec Olivier Laurent) une version "pure" (au sens du lambda-calcul "pur") des réseaux d'interaction différentiels avec connecteurs multiplicatifs et exponentiels, et on donnera une traduction dans ces réseaux du pi-calcul privé - de la somme - de la récursion - de la réplication - du match et du mismatch On verra que cette traduction respecte, en un certain sens, la dynamique du pi-calcul.

Friday 6th July 2007 at 14h Ralph matthes
Substitution - des défis surprenants avec des familles inductives

Abstract: (Hide abstracts)
Des familles inductives de types de données servent bien à représenter le lambda-calcul: le paramètre de la famille décrit l'ensemble de noms de variables libres admises, et le changement du paramètre au cours de la récurrence reflète la génération de noms pour les variables liées. La preuve que cette représentation satisfait les propriétés de base de la substitution - dictées par la théorie de catégories - n'est pas triviale et un travail assez récent (pour Coq, c'était fait par Adams). On veut aller plus loin: On encapsule des sous-expressions de lambda-termes comme si elles n'étaient que des noms de variables libres. Ceci donne le lambda-calcul avec aplatissement explicite. Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont pas offertes par aucun assistant de preuves, or elles pouvaient être encodées dans Coq. Là, déjà la notion d'une occurrence libre d'une variable est un défi pour la conception mathématique. Heureusement, la vérification entière des propriétés de base était abordable dans Coq, le plus grand problème étant un affaiblissement de la règle que la substitution qui remplace chaque variable par le terme qui consiste de cette variable n'a aucun effet.

Friday 6th July 2007 at 10h Khelifa Saber
Soutenance de sa thèse

Abstract: (Hide abstracts)
Le lambda-mu-&-or-calcul est une extension du lambda-calcul associée à la déduction naturelle classique où sont considérés tous les connecteurs. Les principaux résultats de cette thèse sont : - La standardisation, la confluence et une extension de la machine de J.-L. Krivine en lambda-mu-&-or-calcul. - Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures. - Une sémantique de réalisabilité pour le lambda-mu-&-or-calcul qui permet de caractériser le comportement calculatoire de certains termes typés et clos. - Un théorème de complétude pour le lambda-mu-calcul simplement typé. - Une introduction à un lambda-mu-&-or-calcul par valeur confluent.

Thursday 5th July 2007 at 15h Hugo Herbelin (INRIA Futurs),
The hidden exception handler of Parigot's lambda-mu-calculus and its completeness properties

Abstract: (Hide abstracts)
Call-by-name lambda-mu-calculus was proved observationally incomplete by David and Py. Still, Saurin showed that an apparently inoffensive extension of the reduction rules allows to recover Böhm completeness back. We show that this extension corresponds to adding a simple form of exception handler that is commonly called control delimiter. Control operators with delimiters have been studied by Felleisen and by Danvy and Filinski. Typically, Filinski showed that all concrete monads (e.g. references, exceptions, non-determinism, ...) are expressible in call-by-value lambda-calculus with delimited control. This result translates to the case of call-by-value lambda-mu-calculus and suggests that side-effects could be smoothly integrated to the Curry-Howard correspondence.

Abstract available as a PDF file.

Thursday 5th July 2007 at 10h15 Kim Bruce (Pomona College),
Modularity and Scope in Object-Oriented Languages

Abstract: (Hide abstracts)
Language designers for object-oriented languages have tended to use classes as the main modularity boundaries for code. While Java includes packages, they were not particularly well thought-out and have many flaws. However, the designers got very few complaints for the weak design because programmers don't use them very effectively. In this talk we describe some useful properties of modularity and information-hiding mechanisms in object-oriented languages and and present a language design that supports these properties.

Wednesday 4th July 2007 at 14h M Zaionc
Classical and intuitionistic logic are asymptotically identical

Abstract: (Hide abstracts)
This talk considers logical formulas built on the single binary connector of implication and a finite number of variables. When the number of variables becomes large, we prove the following quantitative results: {\em asymptotically, all classical tautologies are \textit{simple tautologies}}. It follows that {\em asymptotically, all classical tautologies are intuitionistic}. We investigate the proportion between the number of formulas of size $n$ that are tautologies against the number of all formulas of size $n$. After isolating the special class of formulas called simple tautologies, of density $1/k+O(1/k2)$, we exhibit some families of non-tautologies whose cumulated density is $1-1/k-O(1/k2)$. It follows that the fraction of tautologies, for large $k$, is very close to the lower bound determined by simple tautologies. A consequence is that classical and intuitionistic logics are close to each other when the number of propositional variables is large.

Wednesday 4th July 2007 at 10h15 M Zaionc
Asymptotic densities in logic

Abstract: (Hide abstracts)
This talk presents numerous results from the area of quantitative investigations in logic and type theory. For the given logical calculus (or type theory) we investigate the proportion of the number of distinguished set of formulas (or types) $A$ of a certain length $n$ to the number of all formulas of such length. We are especially interested in asymptotic behavior of this fraction when $n$ tends to infinity. The limit $\mu(A)$ if exists, is an asymptotic probability of finding formula from the class $A$ among all formulas or the asymptotic density of the set $A$. Often the set $A$ stands for all tautologies of the given logical calculus (or all inhabited types in type theory). In this case we call the asymptotic of $\mu(A)$ the \emph{density of truth}. Most of this research is concern with classical logic and sometimes with its intuitionistic fragments but there are also some attempts to examine modal logics. To do that we use methods based on combinatorics, generating functions and analytic functions of complex variable with the special attention given to singularities regarded as a key determinant to asymptotic behavior.

Thursday 28th June 2007 at 10h15 Michał Pałka
Functional Graphical User Interfaces 151 An Implementation based on GTK

Abstract: (Hide abstracts)
In this talk we try to attack the problem of programming Graphical User Interfaces in a manageable way. User interfaces are an area where traditional, imperative programming techniques lead to unstructured and error prone code. As an antidote for that, many alternative computation models have been proposed, of which the synchronous dataflow model will be our theme. We present a functional GUI toolkit, based on the above model, which does not have many of the drawbacks of traditional toolkits. The toolkit is implemented in Haskell, a functional language which provides a handy base for creating domain-specific languages.

Thursday 21st June 2007 at 10h15 David Aspinall
The Future of Proof Engineering with Proof General

Abstract: (Hide abstracts)
Proof General is a generic proof development environment which has been in use for almost 10 years, providing interface support for interactive theorem prover systems such as Isabelle, LEGO, Coq and PhoX. Recently, a new version has been introduced, called Proof General Kit, which is based on a component framework that is designed to enable much richer interactions, including special manipulations for "Proof Engineering". We see the challenge of Proof Engineering as being necessary to take interactive theorem proving to the next level. Proof Engineering, like Software Engineering, considers the lifecycle of large proof developments. It will provide facilities for the construction, maintenance, and comprehension of large proofs. We want to provide foundations and tools to support Proof Engineering at a generic level, within the Proof General Kit framework. This talk will introduce the Proof General Kit and Proof Engineering. I will explain some of the research problems and early solution ideas for our research programme and explain how they relate to underlying proof assistant engines. The presentation will be at a high level and not overly technical.

Friday 15th June 2007 at 10h30 Graham White
The Semantics of Adverbial Inference

Abstract: (Hide abstracts)
Adverbial inferences, such as that from "he ran quickly" to "he ran", have raised serious problems for the semantics of natural language. Traditionally -- at any rate since Davidson's work -- these inferences have been handled with a first-order formalisation using individual events. This is not without problems: there is, for example, very little consensus about conditions of identity for events. I propose an alternative, higher order semantics, using two categories, and I will discuss its implications for the semantics of such sentences.

Friday 15th June 2007 at 09h Kurt Ranalter
Continuations, events, and natural language

Abstract: (Hide abstracts)
I report on work in progress concerning the development of a natural language parser. On the one hand I discuss how a call-by-value lambda-mu-calculus endowed with labels can be used to provide a Montague semantics for natural language and how events can be exploited in order to deal with linguistic phenomena such as adverbs. On the other hand I explain how a type-driven parser can be obtained by enriching the type system with morphosyntactic and grammatical features.

Thursday 14th June 2007 at 10h15 Laurent Boyer
Densité de propriétés sur les automates cellulaires

Abstract: (Hide abstracts)
Les automates cellulaires sont souvent construits et étudiés pour adopter un comportement précis. On adopte ici un point de vue opposé en s'intéressant aux comportements typiques parmi l'ensemble des AC ou de manière équivalente au comportement des AC aléatoires. A l'aide de méthodes combinatoires variées, et de la complexité de Kolmogorov, on obtient des résultats sur la probabilité de certaines propriétés dynamiques des AC.

Thursday 7th June 2007 at 14h Richard Dapoigny
Vers une planification basée sur une Théorie Constructive des Types en logique Intuitionniste. ATTENTION : C'EST A 14 H

Abstract: (Hide abstracts)
Le travail présenté introduit une nouvelle approche pour la composition automatique de buts en planification en considérant les buts comme des fonctions de leur contexte (i.e., à partir de structures de connaissances sur le domaine). Etant donné un but global et une situation initiale, le modèle de planification peut être généré directement à partir d'un ensemble de buts primitifs via la connaissance du domaine et le raisonnement sur les types de buts. La connaissance sur le domaine est extraite d'une ontologie locale, sélectionnant les entités disponibles et leurs relations. Un processus de raisonnement valide ces informations via un theorem prover en théorie intuitionniste des types (ITT). L'approche proposée bénéficie de l'efficacité du theorem prover à travers ITT combinée à l'expressivité sémantique des ontologies. La representation des connaissances utilise les types d'enregistrements dépendants pour décrire à la fois les types de contextes du domaine et des structures intentionnelles décrivant une action, le but à réaliser et ses effets. Les types d'enregistrements dépendants capturent une connaissance partielle du domaine et possèdent un impact computationnel immédiat.

Friday 1st June 2007 at 10h15 Sébastien Briais
Une bisimulation ouverte pour le spi calcul

Abstract: (Hide abstracts)
Dans le cadre du pi calcul, la bisimulation ouverte est une notion d'équivalence attractive car elle offre de bonnes propriétés de congruence et est assez facile à implémenter. Nous proposons une généralisation de cette notion dans le cadre du spi calcul, une extension du pi calcul permettant de raisonner sur les protocoles cryptographiques.

Thursday 31st May 2007 at 10h15 Colin Riba (LORIA),
Strong Normalization and Union Types

Abstract: (Hide abstracts)
When enriching the lambda-calculus with rewriting, union types may be needed to type all strongly normalizing terms. However, with rewriting, the elimination rule (UE) of union types may also allow to type non normalizing terms (in which case we say that (UE) is unsafe). This occurs in particular with non-determinism, but also with some confluent systems. It appears that studying the safety of (UE) amounts to the characterization, in a term, of safe interactions between some of its subterms. We study the safety of (UE) for an extension of the lambda- calculus with simple rewrite rules. We prove that the union and intersection type discipline without (UE) is complete w.r.t. strong normalization. This allows to show that (UE) is safe if and only if an interpretation of types based on biorthogonals is sound for it.

Thursday 10th May 2007 at 10h15 Christophe Raffalli
Les preuves en PML

Abstract: (Hide abstracts)
Nous montrerons comment un langage similaire à ML, peut être transformé de manière très simple et minimaliste en un système de déduction où les preuves sont des programmes.

Thursday 19th April 2007 at 10h15 Guillaume Theyssier (Univ. Savoie),

Abstract: (Hide abstracts)
Considérez la suite (ordonnée) de fractions suivante: 17/91 78/85 19/51 23/38 29/33 77/29 95/23 77/19 1/17 11/13 13/11 15/2 1/7 55/1. Partez de l'entier 2 et à chaque étape multipliez l'entier courant par la première fraction pour laquelle le produit est entier et répétez le processus. Les puissances de 2 que vous obtenez sont exactement les 2^p où p est premier. C'est un simple exemple de programme d'un langage de programmation universel: FRACTRAN. Après avoir expliqué en quoi FRACTRAN est une présentation originale et concise de modèles de calculs bien connus, nous montrerons deux résultats d'indécidabilité sur les problèmes de Collatz généralisés qui sont des corollaires faciles de l'universalité de FRACTRAN. Tout ces résultats sont tirés d'un article de Conway de 86.

Thursday 5th April 2007 at 10h15 Dominique Duval (UJF),
Homomorphismes de logiques

Abstract: (Hide abstracts)
On connaît les homomorphismes de monoïdes, de groupes, mais qu'est-ce qu'un homomorphisme de logiques ? Pour répondre à cette question, nous avons introduit avec Christian Lair en 2002 la notion de "propagateur", qui est définie de façon très simple à partir des "esquisses" de Charles Ehresmann. Le but de l'exposé est de présenter les esquisses et les propagateurs, et de montrer comment un propagateur définit une "logique", avec des modèles et un système de preuves, apparentée aux "doctrines" de William Lawvere. La définition des homomorphismes de logiques est alors évidente. Je parlerai aussi d'une application à la sémantique des effets de bord dans les langages de programmation, qui constitue ma motivation initiale pour ces travaux. Les quelques notions de théorie des catégories nécessaires à la compréhension de tout cela seront rappelées dans l'exposé.

Thursday 29th March 2007 at 10h Silvia Ghilezan (University of Novi Sad),
Characterizing strong normalization in the Curien Herbelin

Abstract: (Hide abstracts)
In this talk, I will present an intersection type system for Curien Herbelin symmetric lambda calculus, that has been developed in the joint work with Dan Dougherty and Pierre Lescanne. The system completely characterizes strong normalization of the free (unrestricted) reduction. The proof uses a technique based on fixed points. The system enjoys subject reduction and subject expansion.

Thursday 22nd March 2007 at 10h15 Julien Narboux
Formalisation et automatisation du raisonnement géométrique en Coq

Abstract: (Hide abstracts)
Je présenterai d'abord un développement formel à propos des fondements de la géométrie. Celui-ci consiste en la formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie. Ensuite, je décrirai l'implantation en Coq d'une procédure de décision pour la géométrie affine plane: la méthode des aires de Chou, Gao et Zhang. Dans la troisième partie, nous nous intéresserons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof ( GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq. Enfin, je presenterai un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.

Thursday 15th March 2007 at 10h15 Francois Lamarche (LORIA),
Sémantiques symétriques des preuves en logique propositionnelle classique

Abstract: (Hide abstracts)
Nous savons maintenant qu'il existe dans la nature des modèles de la logique classique qui sont aux catégories ce que les algèbres de Boole sont aux ensembles ordonnés. Durant des années on a cru que de tels êtres ne pouvaient exister, étant donné le célèbre 171 paradoxe de Joyal 187 : une catégorie cartésienne fermée ne peut être équipée d'une négation symétrique. Les premiers exemples étaient des catégories de réseaux de démonstrations. Nous avons ensuite construit des sémantiques dénotationnelles pour la logique classique qui ressemblent beaucoup aux espaces cohérents. L'exposé se concentrera sur les propriétés essentielles que tous ces modèles possèdent, en d'autres termes sur les raisons pour quoi ça marche. Ces modèles nous mènent à nous poser des questions sur l'universalité de l'isomorphisme de Curry-Howard : il existe des façons de dénoter des preuves en logique classique pour lesquelles le processus de normalisation ne correspond pas au calcul en programmation fonctionnelle. Les connaissances en théorie des catégories que nous supposons de la part de l'autitoire sont absolument minimales : les définitions de catégorie, foncteur et transformation naturelle.

Tuesday 13th March 2007 at 10h15 Lionel Vaux (IML),
λ-calcul algébrique

Abstract: (Hide abstracts)
On propose une extension naturelle du λ-calcul autorisant la formation de combinaisons linéaires de termes. Ceci reflète dans la syntaxe la sémantique quantitative du λ-calcul simplement typé dans les espaces de finitude, où les types sont interprétés par des espaces vectoriels particuliers, et les λ-termes par des fonctions entre ces espaces.
On étudie les effets de la présence de coefficients scalaires sur la réduction: après avoir étendu la β-réduction en une relation contextuelle et confluente, on s'intéresse à la cohérence du calcul et à des propriétés de normalisation dans un cadre typé.
On établit enfin une correspondance entre ce λ-calcul algébrique et le λ-calcul linéaire-algébrique d'Arrighi et Dowek en montrant qu'ils correspondent à deux stratégies de réduction (par nom et par valeur) d'une syntaxe commune.

Thursday 8th March 2007 at 10h15 Lionel Vaux
Un lambda-bar-mu calcul avec produit de convolution sur les piles

Abstract: (Hide abstracts)
On présente une extension du lambda-bar-mu calcul de Herbelin avec une opération binaire sur les piles (ou contextes), qui peut aussi être interprétée comme un opérateur de choix non déterministe. Les règles de réduction associées dotent cette opération de propriétés similaires à celles du produit de convolution sur les distributions. C'est la version lambda-calculesque d'une extension par polarisation des réseaux d'interaction différentiels d'Ehrhard-Régnier: on met ce fait en évidence grâce à une sémantique dénotationnelle dans la catégorie des ensembles et relations.

Thursday 1st March 2007 at 10h15 Alexandre Miquel
Un lambda-calcul avec constructeurs

Abstract: (Hide abstracts)
Dans cet exposé, je présenterai une extension du lambda-calcul dans laquelle le filtrage s'effectue à l'aide d'une construction "case" (analyse par cas au sens du langage Pascal) se propageant à travers les fonctions comme une substitution linéaire de tête. Je montrerai en particulier que cette présentation du filtrage permet de récupérer toute l'expressivité du filtrage à la ML (avec des constructeurs non constants) et même plus. Ensuite, je présenterai la preuve du théorème de Church-Rosser, basée sur une technique inédite de "divide and conquer" dans laquelle on détermine de manière semi-automatique l'ensemble des paires de sous-systèmes qui commutent (en considérant toutes les combinaisons possibles des 9 règles de réduction primitives). Enfin, je montrerai que le calcul vérifie une propriété de séparation (non typée) dans l'esprit du théorème de Böhm.

Thursday 22nd February 2007 at 10h Louis Mandel
Programmation réactive en Caml : Implantation de ReactiveML

Abstract: (Hide abstracts)
ReactiveML est un langage de programmation dédié à la programmation de systèmes réactifs (e.g., simulation de systèmes dynamiques, interfaces graphiques, jeux video). Il est fondé sur le modèle "réactif synchrone" introduit par F. Boussinot. Ce modèle permet de combiner les principes de la programmation synchrone (composition parallèle synchrone de processus, communication par diffusion) et des mécanismes de création dynamique. Le langage est une extension conservative de Ocaml. Il ajoute des constructions supplémentaires pour décrire les comportements temporels des systèmes. Les programmes sont statiquement typés puis traduits en Ocaml. La première partie de cet exposé sera consacrée à la présentation du langage. La seconde partie présentera son implantation.

Thursday 15th February 2007 at 14h R Kervarc
Soutenance de sa thèse

Abstract: (Hide abstracts)

Thursday 8th February 2007 — Friday 09 february 2007
Groupe de Travail LAC du DGR IM

Abstract: (Hide abstracts)

Thursday 8th February 2007 GDR IM
Journées Logique, Algèbre et Calcul du GDR IM

Abstract: (Hide abstracts)
Les 8 et 9 Février 2007 auront lieu, à Chambéry, les rencontres du groupe LAC du GDR IM. Plus d'info sur la page de ces journées :

Thursday 1st February 2007 at 11h Groupe de lecture topos
Sous-faisceaux dans les topologies de Grothendieck

Abstract: (Hide abstracts)
Sous-faisceaux dans les topologies de Grothendieck et si on a le temps topologies de Lawvere-Tierney

Thursday 25th January 2007 at 10h15 Pierre Lescanne
Jeux, équilibres et réseaux de régulation de gènes

Abstract: (Hide abstracts)
La théorie des jeux peut être vue comme la théorie des équilibres. Comme elle est un peu plus que cinquantenaire, il peut sembler opportun de la réexaminer. C'est ce que nous faisons en proposant une nouvelle vision plus générale que nous appelons 171jeux à conversion-préférence187, en abrégé 171jeux CP187. Ce formalisme semble s'adapter agréablement aux réseaux de régulation de gênes.

Thursday 18th January 2007 at 14h Radu Mateescu (INRIA Rhône Alpes),
MCL: A Model Checking Language for Concurrent Value-Passing Systems

Abstract: (Hide abstracts)
Model checking is a successful technique for verifying automatically temporal properties of concurrent finite-state programs represented as Labelled Transition Systems (LTSs). Among the various formalisms used for specifying properties, an outstanding candidate is the modal mu-calculus, a very powerful fixed point-based temporal logic. However, in spite of its theoretical expressiveness, standard modal mu-calculus is a too low-level formalism for end-users, making the specification of complex properties tedious and error-prone. In this talk, we propose MCL (Model Checking Language), an extension of the modal mu-calculus with high-level, data-based constructs inspired from programming languages, which substantially increase its expressive power as well as the conciseness and readability of properties. We also present an on-the-fly model checking method for verifying MCL formulas on LTSs, based upon translating the verification problem into the resolution of a boolean equation system. The MCL language and the associated verification method are supported by the EVALUATOR 4.0 model checker, developed within the CADP verification toolbox using the generic OPEN/CAESAR environment for on-the-fly exploration of LTSs.

Thursday 18th January 2007 at 10h15 Guillaume Melquiond
De l'arithmétique d'intervalles à la certification de programmes

Abstract: (Hide abstracts)
Parce que les nombres manipulés en machine ont généralement un domaine et une précision limités, il est nécessaire de certifier soigneusement que les applications les utilisant se comportent correctement. Réaliser une telle certification à la main est un travail propice à de nombreuses erreurs. Les méthodes formelles permettent de garantir l'absence de ces erreurs, mais le processus de certification est alors long, fastidieux et généralement réservé à des spécialistes. Le travail présenté dans cet exposé vise à rendre ces méthodes accessibles en automatisant leur application. L'approche adoptée s'appuie sur une arithmétique d'intervalles accompagnée d'une base de théorèmes sur les propriétés des arithmétiques approchées et d'un mécanisme de réécriture d'expressions permettant le calcul de bornes fines sur les erreurs d'arrondi. Ce travail s'est concrétisé par le développement de l'outil Gappa d'aide à la certification. Il permet de vérifier les propriétés de codes numériques qui utilisent de l'arithmétique à virgule fixe ou à virgule flottante. Cette vérification s'accompagne de la génération d'une preuve formelle de ces propriétés utilisable par l'assistant de preuves Coq. Cette preuve s'appuie sur une bibliothèque de propriétés arithmétiques et elle contient principalement des calculs entiers qui reflètent les calculs par intervalles effectués par l'outil. Cependant, pour que la preuve soit d'une taille raisonnable, Gappa élimine les lemmes inutiles et simplifie les nombres que Coq aura à manipuler. Gappa a été utilisé avec succès pour certifier la correction de fonctions dans les bibliothèques CRlibm, CGAL et FLIP par exemple.

Thursday 11th January 2007 at 10h15 G Lafitte
Du calcul à l'incomplétude

Abstract: (Hide abstracts)
Nous parlerons de calculabilités généralisées permettant de définir de nouvelles complexités à la Kolmogorov-Chaitin et de préciser les liens entre incomplétude et calcul.

Thursday 14th December 2006 at 11h Philippe Audebaud
Vérification formelle d'algorithmes probabilistes dans coq

Abstract: (Hide abstracts)
Cet exposé s'appuit sur le langage lambdaO (Park, Pfenning et Thrun), un langage fonctionnel typé pur étendu avec une notion de variable aléatoire. C'est un travail commun avec Christine Paulin. Après en avoir donné une présentation succinte, et illustré son pouvoir expressif, nous abordons des aspects sémantiques. Nous en proposons une sémantique dénotationnelle directe, à partir de laquelle nous produisons mécaniquement un système d'inférence pour la sémantique axiomatique à la Hoare. Des exemples de preuves en correction partielle sont proposés ; la correction totale est abordée, mais le cadre formel n'est pas complet à ce jour. Enfin, nous indiquerons comment la vérification d'algorithmes (fonctionnels) probabilistes est envisagée dans la suite de notre travail.

Thursday 7th December 2006 at 10h15 Guillaume Theyssier
Attention, une Conwayrie peut en cacher une autre.

Abstract: (Hide abstracts)
En recherchant des résultats sur la suite de Conway et le (fameux ?) théorème cosmologique, Pierre est tombé sur un article pour le moins intrigant du même monsieur. Considérez la suite (ordonnée) de fractions suivante : 17/91 78/85 19/51 23/38 29/33 77/29 95/23 77/19 1/17 11/13 13/11 15/2 1/7 55/1 Partez de l'entier 2 et à chaque étape multipliez l'entier courant par la première fraction pour laquelle le produit est entier et répétez le processus. Vous obtenez la suite des 2^p où les p sont les nombres premiers consécutifs. Un miracle pensez vous ? Non, un simple exemple de programme d'un langage de programmation universel : FRACTRAN.

Wednesday 6th December 2006 at 09h A Ranta
Grammars as Software Libraries

Abstract: (Hide abstracts)
Libraries are a major instrument of software engineering, making it possible to reuse code and to distribute labour between programmers with different areas of expertise. The sophisticated application programs we have today would not be possible without huge libraries in areas such as data structures, numerical analysis, signal processing, and computer graphics. Grammars of natural languages are a domain of a lot of expert knowledge, which it would be useful to find in software libraries. However, typical implementations of grammars are monolithic application programs, such as parsers tuned to a particular corpus. New applications typically have to build their grammars from scratch, which makes it costly to build programs such as natural-language interfaces, or to perform high-quality software localization. This talk presents an approach where grammars can be used as libraries for new grammars and for programs that involve natural language components. The approach is implemented in GF (Grammatical Framework), which is a special-purpose functional programming language for writing grammars. Several features of GF are used in an essential way: the division between abstract and concrete syntax; the module system, including parametrized modules; the type system, which is able to enforce grammar checking via type checking; and code generation that makes GF grammars usable in other programming languages, such as C, Haskell, and Java. To bring the discussion to concrete level, we introduce the GF Resource Grammar Library, which implements the basic grammars of ten languages and makes them accessible to non-linguist application programmers. As an application, we show how the library can be used in building a natural-language interface to a proof system.

Tuesday 5th December 2006 at 14h Patrick Thévenon
Soutenance de thèse : Vers un assistant de preuve en langue naturelle

Abstract: (Hide abstracts)
Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérication de démonstrations mathématiques écrites en langue naturelle. L'architecture générale du système se décrit en 4 phases : 1. analyse de la démonstration par des outils linguistiques ; 2. traduction de la démonstration dans un langage restreint ; 3. interprétation du texte traduit en un arbre de règles de déduction ; 4. validation des règles de déduction à l'aide d'un démonstrateur automatique. Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens. Cette thèse présente plus en détail ce projet et développe principalement les points suivants : - définition du langage restreint et de son interprétation ; - propriétés du type principal de termes d'un lamlbda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ; - description du démonstrateur automatique.

Thursday 30th November 2006 at 14h Frédéric Ruyer
Soutenance de thèse : Preuves, Types et Sous Types

Abstract: (Hide abstracts)
Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST développé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types en se basant sur des treillis complets comportant des propriétés additionnelles permettant d'interpréter types et termes;puis nous étudions diverses propriétés théoriques du système telles que la réduction du sujet ainsi que son expressivité à travers des exemples traitant de la possibilité ou de l'impossibilité de définir des notions-clés de la logique et de l'informatique théorique. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches issus de l'informatique dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Thursday 30th November 2006 at 10h15 Gilles Dowek
Les algèbres de valeurs de vérités et la normalisation

Abstract: (Hide abstracts)
On propose une notion de modèle pour la logique intuitionniste, qui étend celle fondée sur les algèbre de Heyting. Cette notion de modèle permet de distinguer l'équivalence logique (si A est démontrable, alors B aussi, et vice-versa) de l'équivalence calculatoire (toute démonstration de A est une démonstration de B, et vice-versa), ce que ne permettaient pas de faire les algèbres de Heyting. On montre ensuite que cette notion de modèle peut être utilisée pour démontrer la normalisation des démonstrations dans de nombreuses théories comme l'arithmétique de Peano ou la logique d'ordre supérieur.

Thursday 16th November 2006 at 10h15 K Ranalter
Categories for Pragmatics

Abstract: (Hide abstracts)
In this talk we present a categorical proof theory for a logic for pragmatics. The aim of this logic is to provide a framework that allows to formalize reasoninig about the pragmatic force with which a sentence may be uttered. The concept of pragmatic force comes from speech act theory and plays a crucial role also in certain branches of artificial intelligence, in particular in the developement of communication protocols for software agents. Instead of considering the full-blown theory of speech acts we focus here on speech acts that either have the pragmatic force of an assertion or the pragmatic force of an obligation, and on how these speech acts can be related to each other. In particular, we are interested in a principle proposed by Bellin and Dalla Pozza that allows the propagation of obligations through causal chains of assertions. The study of such principles from the point of view of categorical proof theory is a nontrivial task and we discuss some of the issues that need to be considered in order to get soundness and completeness results.

Thursday 26th October 2006 at 10h15 P Hyvernat
Introduction aux jeux de Conway et nombres surréels ; problèmes de combinatoire.

Abstract: (Hide abstracts)
Conway a grandement participé à l'élaboration de la théorie des nombres surréels et à la théorie des jeux à deux personnes. Rapidement, un nombre surréel peut-être vu comme un jeu (potentiellement infini) très inintéressant. À cause de cette différence, les deux théories se sont depuis développées de manière quasi indépendante. Je présenterais d'abord le noyau commun aux nombres surréels et aux jeux. Ceci expliquera notamment comment il est possible d'obtenir la moitie d'un coup d'avance sur son adversaire. (Obtenir un tiers de coup d'avance est nettement plus complexe !) Je passerais ensuite à la théorie des jeux impartiaux (style Nim) dont la théorie, plus ancienne, est comprise dans la précédente. Le but est de présenter (prouver ?) le théorème de Sprague-Grundy ainsi que la conjecture sur les jeux octaux. Si le temps et l'assistance le permettent, je présenterai les avancées récentes autour des jeux impartiaux où l'on inverse gagnant et perdant (convention de 171 misère 187). Pour les survivants, je pourrais même parler (peut-être pendant le repas) de la catégorie de jeux due à André Joyal : c'est probablement la toute première catégorie monoidale close de jeux / stratégies. (Malheureusement, elle ne permet pas de modéliser la logique linéaire...) Je ne présenterais rien de nouveau dans cet exposé. Il s'agit en quelque sorte d'une publicité vantant les joies insoupçonnées de la combinatoire des jeux. Idéalement, une ou deux personnes auront envie de m'accompagner pour aller regarder un peu plus loin...

Thursday 19th October 2006 at 10h15 travail collectif
groupe de travail sur un resultat de Gandy

Abstract: (Hide abstracts)
Nous chercherons à comprendre la preuve de forte normalisation du lambda calcul simplement typé (et de certaines extensions : système T de Godel, ajout d'un produit, ...) faite par Gandy. Il semble que cette preuve utilise une mesure (entière ?) qui décroit par réduction.

Thursday 12th October 2006 at 11h Aurelien Pardon
Une explication du critere de Danos-Regnier pour MLL

Abstract: (Hide abstracts)
Les représentations graphiques des preuves de la logique linéaire, les proof-nets, permettent de s'abstraire de contraintes inhérentes au calcul des séquents comme la syntaxe et les règles structurelles. La correction (ou prouvabilité) de tels réseaux peut se vérifier à l'aide de critères purement graphiques, comme le critère de Danos-Regnier. Sa simplicité en fait le rend très efficace mais peu compréhensible. Pour donner une preuve de complétude d'un tel critère et tenter de l'expliquer, nous utiliserons une logique différente : MILL. Dans ce système intuitionniste, les règles logiques sont des règles de typage d'un lambda-calcul et les réseaux de preuves ses arbres de syntaxe. Le critère de Danos-Regnier nous permettra de construire un lambda-terme typable à partir du réseau de preuve, assurant ainsi sa validité.

Thursday 5th October 2006 at 10h15 F Becker
Pavages auto-assemblants : un calcul géométrique

Abstract: (Hide abstracts)
Les pavages auto-assemblants sont un modèle de calcul introduit par Winfree en 2000 afin d'étudier les phénomènes d'auto-assemblage, naturels et artificiels. Je présenterai ce modèle de calcul, d'abord sa définition, puis deux constructions importantes en programmation, le passage paramètre <-> argument (théorème s-n-m) et la récursion, dont nous verrons qu'elles sont assorties de contraintes géométriques pas toujours triviales. Nous verrons ces deux notions appliquées dans des jeux de tuiles simples, l'un qui implémente les homothéties, et l'autre qui assemble le pavage de Robinson (un pavage quasi- périodiques). Nous examinerons aussi les limites du modèle, qui sont de deux sources, l'une géométrique, avec des problèmes de type dead-lock qui rappellent le parallélisme, l'autre rattachée à la complexité Turing. Si le temps le permet, je présenterai des idées de graphes de Cayley qui permettent de s'affranchir de ces limites.

Thursday 28th September 2006 at 10h15 G Theyssier
Automates cellulaires et systèmes dynamiques

Abstract: (Hide abstracts)
Dans cet exposé, je parlerai des automates cellulaires vus comme des systèmes dynamiques et sous l'angle de propriétés topologiques classiques comme la (non-)sensibilité aux conditions initiales et l'expansivité. Je présenterai la classification de Kurka basée sur ces propriétés dans la topologie de Cantor et son interprétation en terme de circulation de l'information. Cette classification a le défaut de ne pas être invariante par décalage ce qui la rend artificielle pour les automates cellulaires. Le reste de l'exposé sera consacré à une approche récente pour résoudre ce problème : reprendre les différents modes de circulation de l'information de cette classification mais en les étendant à toutes les directions dans l'espace-temps. Cette dernière partie contiendra des résultats de M. Sablik mais aussi une petite collection de questions ouvertes.

Thursday 21st September 2006 at 10h15 Christophe Raffalli
PhoX et après ?

Abstract: (Hide abstracts)
J'exposerai mes idées pour une nouvelle sorte de théorème prouveur, basé sur les idées suivantes: - on crée le langage de programmation avec un système de typage statique fort le plus fort possible - on étend ce langage pour en faire une logique (on n'ajoute pas la logique au dessus du langage) Le but de ce séminaire sera de démarrer un éventuel groupe de travail ...

Thursday 29th June 2006 at 10h15 Karim Nour
Une sémantique de réalisabilité pour un système de type avec intersection et variables d'expansion.

Abstract: (Hide abstracts)
Je presente dans mon exposé le système de type avec intersection de J. Wells qui permet de trouver le type principal d'un lambda-terme uniquement avec l'opération "substitution". Pour cela, il ajoute d'autres variables de type dites "variables d'expansion" et definit la substitution sur ces variables. Je vous présente ensuite une sémantique de réalisabilité pour ce système et un théorème de complétude pour un de ses sous systemes. Ce travail a été fait en collaboration avec F. Kamareddine et J. Wells.

Thursday 22nd June 2006 at 10h15 Noel Bernard
Introduction aux Bigraphes

Abstract: (Hide abstracts)
Parmi les modèles de la concurrence et de la mobilité qui ont foisonné après la définition par Milner du Pi-Calcul, on rencontre deux familles très différentes: les modèles de la communication, qui prolongent directement le Pi-Calcul , et des modèles basés sur une notion spatiale de lieux ou de places, dont un exemple bien connu est les Ambients de Cardelli et Gordon. Les Bigraphes, proposés récemment par Milner, sont une tentative d'englober ces deux courants dans une structure unique. Nous proposons une introduction aux Bigraphes, basée sur le tutoriel que Milner a présenté à Paris en septembre dernier.

Thursday 15th June 2006 at 10h15 François Régis Sinot
Stratégies du lambda-calcul dans les réseaux d'interaction

Abstract: (Hide abstracts)
Le lambda-calcul a deux modèles d'implantation principaux: les machines abstraites, utilisées pour l'appel par nom, par valeur, etc., et les réseaux d'interaction, utilisés pour la réduction optimale, les évaluateurs à la Mackie, etc. La nature très distribuée des réseaux d'interaction ne permet pas, en général, de décrire précisément la stratégie qu'ils implantent et ces deux modèles d'implantation semblent complètement déconnectés. J'établis une connexion entre ces deux mondes en proposant des traductions des stratégies habituelles du lambda-calcul dans les réseaux d'interaction. Ces traductions reposent sur l'idée très simple d'introduire un jeton d'évaluation qui séquentialise certaines réductions. Les stratégies traitées sont l'appel par nom, par valeur, par nécessité et la stratégie "fully lazy".

Thursday 8th June 2006 at 10h15 Laurent Vuillon
Combinatoire et mots de Sturm

Abstract: (Hide abstracts)
Nous aborderons diverses méthodes de combinatoire des mots appliquées aux mots de Sturm. En particulier, nous démontrerons des théorèmes de base de la combinatoire des mots comme le lien entre complexité et périodicité, l'équivalence entre plusieurs définitions des mots de Sturm et enfin des résultats sur les graphes des mots (graphes de De Bruijn ou de Rauzy) et la dynamique de ces graphes pour les mots de Sturm.

Thursday 11th May 2006 at 14h Laurent Regnier (Université de la Méditerranée),

Abstract: (Hide abstracts)
TBA. Slogan: comment utiliser la machine de Krivine pour linéariser les lambda-termes et rapport avec la propriété d'uniformité du lambda-calcul diff.

Thursday 27th April 2006 at 10h Olivier Laurent (en cours de negociation)?

Abstract: (Hide abstracts)

Thursday 13th April 2006 at 10h15 Khelifa Saber
Un résultat de complétude pour une classe de types du système F

Abstract: (Hide abstracts)
On définit une sémantique de réalisabilité inspirée des candidats de réductibilité de J.Y. Girard et adaptée par M. Parigot pour le cas classique. On prouve un lemme de correction pour cette sémantique. On montre ensuite la complétude pour une classe de type notée D^+. Cette classe est formée des types qui ne contiennent pas de quantificateurs à droite d'une flèche (i.e. les quantificateurs ne sont qu' à gauche des flèches). Elle contient donc, en particulier, les types de données. C'est une sous classe des types forall positifs pour lesquels la complétude n'est pas vraie (on fournit un contre exemple).

Thursday 6th April 2006 at 10h15 Hugo Herbelin
Au coeur de la dualité du calcul : appel par nom, appel par valeur et calcul des séquents

Abstract: (Hide abstracts)
Nous montrons comment le dédoublement de la règle d'axiome du calcul des séquents de Gentzen permet de mettre en évidence un noyau de calcul qui exprime de manière syntaxique la dualité entre les notions standard d'appel par nom et d'appel par valeur. D'un point de vue théorie de la démonstration, on en conclut que l'appel par valeur est intrinséquement partie prenante de l'interprétation calculatoire du calcul des séquents. D'un point de vue théorie du calcul, on débouche sur un nouveau formalisme basé sur une profonde symétrie entre termes et contextes d'évaluation.

Thursday 30th March 2006 at 14h Julien Moncel
Identification de sommets dans les graphes. (Attention : 14h)

Abstract: (Hide abstracts)
Les codes identifiants ont été introduits pour modéliser un problème de détection de défaillances dans des réseaux multiprocesseurs [1]. C'est un sujet récent de théorie des graphes, qui, dans une de ses variantes, se définit comme suit : étant donné un graphe G=(V,E), un code t-identifiant de G est un sous-ensemble de sommets C de V tel que tout sous- ensemble d'au plus t sommets de G soit identifié de façon unique par la trace de C sur son voisinage fermé. Formellement, C est un code t-identifiant de G si et seulement si on a N[X]cap C neq N[Y]cap C pour toute paire (X, Y) de sous-ensembles distincts d'au plus t sommets de G, où N[X] désigne l'union de X et des voisins de X dans G. Ce sujet peut être vu comme un cas particulier de problème de couverture par tests sur un ensemble structuré. Les problèmes de couverture par tests sont une large classe de problèmes combinatoires, englobant le fameux problème des fausses pièces ou les jeux populaires de devinettes. Lorsqu'un tel code existe, le problème d'optimisation discrète sous-jacent consiste à déterminer un code t-identifiant de cardi- nalité minimum. Au niveau algorithmique, ce problème est NP- difficile [2] . Dans [1], des bornes générales sont données. On peut s'intéresser à l'aspect extrémal de ce problème, en particulier on peut étudier le problème suivant : étant donné un entier n, quels sont les graphes admettant un code t-identifiant de cardinalité minimum parmi les graphes à n sommets ? Dans cet exposé je vais présenter différentes approches pour aborder cette question de combinatoire extrémale. J'exposerai tout d'abord une approche probabiliste, utilisant la notion de graphe aléatoire, qui nous permet d'obtenir une borne supérieure proche de la borne inférieure générale de [1]. Ensuite, j'expose- rai les liens étroits que l'on peut établir entre les codes identifiants et d'autres types de codes, en particulier les codes superimposés, ce qui nous permettra d'obtenir une borne inférieure améliorant celle de [1]. Enfin, je présenterai des constructions basées sur des plans projectifs. Références : [1] M. G. Karpovsky, K. Chakrabarty, L. B. Levitin, On a New Class of Codes for Identifying Vertices in Graphs, IEEE Transactions on Information Theory 44(2), 599-611 (1998). [2] I. Charon, O. Hudry, A. Lobstein, Minimizing the size of an identifying or locating-dominating code in a graph is NP-hard, Theoretical Computer Science 290(3), 2109-2120 (2003).

Thursday 30th March 2006 at 10h15 Guillaume Theyssier
Automates cellulaires : de l'objet syntaxique au système dynamique

Abstract: (Hide abstracts)
Les automates cellulaires sont des systèmes dynamiques discrets composés de cellules agencées régulièrement et qui interagissent localement. Bien que les interactions locales soient très simples à décrire, le comportement du système dans son ensemble est très difficile à prévoir. Dans cet exposé, je présenterai d'une part une approche formelle, basée sur des pré-ordres de simulation, pour comparer et classifier les dynamiques globales de ces objets. Je montrerai comment des classes d'automates définies par des propriétés dynamiques classiques se traduisent dans la structure de ces pré-ordres. Je présenterai également une construction qui permet d'obtenir divers ordres-induits remarquables de certains pré-ordres de simulation, ainsi qu'un automate cellulaire intriguant, capable de simuler le comportement d'une machine de Turing avec un nombre fini arbitrairement grand de têtes de calcul, mais qui interdit la cohabitation simultannée d'un nombre infini de têtes. J'aborderai d'autre part les automates cellulaires comme des objets syntaxiques et étudierai la densité de diverses propriétés de ces objets. Je montrerai comment une contrainte syntaxique locale permet de définir une classe (les automates cellulaires captifs) dans laquelle les propriétés monotones suivent une loi zéro-un. En particulier je montrerai que, dans cette classe, la propriété d'être intrinsèquement universel a une densité 1 tout en étant indécidable.

Monday 27th March 2006 at 10h15 Olivier Brunet
Éléments d'une logique de la connaissance quantique (Attention, c'est un lundi)

Abstract: (Hide abstracts)
La logique quantique, qui est une composante importante des travaux visant à la compréhension du monde quantique, reste mal comprise et difficilement utilisable en pratique. Grâce à la mise en évidence de l'importance de notions "classiques" comme les points de vue ou la connaissance partielle, nous montrons comment il est possible d'obtenir de nouvelles pistes pour l'étude de ce type de logique, avec en particulier des méthodes de recherche automatique de preuves. Dans cet exposé, nous présenterons un ensemble de résultats nous effectuerons une présentation de la logique quantique ainsi que le modèle usuel de cette logique, à savoir les treillis orthomodulaires. Ensuite, nous exposerons une approche utilisant les "systèmes de représentation" (développés par l'auteur durant sa thèse de doctorat, voir bibliographie) basée sur les notions de connaissance partielle et de points de vue qui permet de fournir une caractérisation purement classique et non probabiliste (basée sur l'utilisation d'algèbres booléennes). Nous montrerons enfin comment cette caractérisation permet d'envisager la logique quantique d'une nouvelle manière, et fournir de nouveaux outils pour son étude. En particulier, nous présenterons un fragment décidable de cette logique, sous forme de calcul des séquents. Références:

Thursday 23rd March 2006 at 14h15 Julien Forest
Réécriture d'ordre supérieur avec motifs. (Attention : 14h15)

Abstract: (Hide abstracts)
Dans cet exposé nous présenterons deux formalismes de réécriture d'ordre supérieur permettant l'utilisation de filtrage "à la ML". Le premier de ces formalismes, le lambda P calcul, est une extension du calcul lambda sigma traitant de manière complètement explicite les notions de substitution et de filtrage. Nous montrerons qu'il possède les propriétés de normalisation forte sur les termes typés et de confluence. Le second formalisme est un formalisme de réécriture d'ordre supérieur fondé sur les (S)ERS. Ce formalisme autorise la définition de systèmes de réécriture utilisant la notion de filtrage. Nous donnerons un critère syntaxique de confluence pour de tels systèmes.

Thursday 16th March 2006 at 10h15 Nicolas Bedaride
Complexité du billard polyédral

Abstract: (Hide abstracts)
On considère un polyèdre, on définit alors le billard polyédral de la facon suivante: On part d'un point d'une face, on se donne une direction et on se déplace dans cette direction jusqu'à rencontrer une autre face. On obtient un nouveau point, la direction est alors réfléchie orthogonalement par rapport à cette face. Pour étudier cette application on repère chaque face par une lettre, l'orbite d'un point devient une suite de lettres. C'est ce qu'on appelle un mot. Le but est d'étudier ces mots grace en autre à leurs fonctions de complexité. Nous présenterons les estimations connues pour un polyèdre général, et nous nous intéresserons plus précisemment au cas du cube.

Thursday 9th March 2006 at 10h15 Emmanuel Beffara
Modèles concurrents de la logique linéaire

Abstract: (Hide abstracts)
Dans cet exposé, on développera une interprétation de la logique linéaire en termes de processus concurrents. On utilise pour cela une variante du pi-calcul, munie d'une notion paramétrable d'observation (divergence, may- ou must-testing...), d'où l'on déduit une notion abstraite de comportement. La structure de ces comportements mène à la définition de connecteurs logiques, inspirés des logiques spatiales et temporelles, qui décrivent les propriétés fondamentales des processus. Le système obtenu est une forme de logique linéaire qui définit pour le pi-calcul un système de type qui garantit de bonnes propriétés comme la terminaison et l'absence de blocage. D'autre part, ce système de type établit une correspondance à la Curry-Howard entre la concurrence et diverses variantes de logique linéaire, qui s'intègre bien aux précédentes études sur la décomposition du calcul fonctionnel dans les calculs concurrents.

Thursday 9th February 2006 at 14h Yves Guiraud
Polygraphes, réécriture et logique (Attention : 14h)

Abstract: (Hide abstracts)
Dans cet exposé, je présenterai la structure de polygraphe, une sorte de complexe cellulaire, à travers ses liens avec la réécriture et la logique. Dans la première partie, nous verrons comment tout système de réécriture de termes peut être traduit sous la forme d'un polygraphe, vu ici comme un système de réécriture de circuits. Sur un exemple, je montrerai comment construire des ordres de terminaison adaptés à ces objets. Dans la seconde partie, nous traduirons le calcul propositionnel et ses démonstrations en un polygraphe : cela permet d'obtenir des représentations bidimensionnelles pour les formules et tridimensionnelles pour les démonstrations. Enfin, si le temps le permet, je parlerai d'une piste menant à une autre description polygraphique des démonstrations classiques, toujours en trois dimensions.

Thursday 2nd February 2006 at 14h Damien Jamet
Combinatoire des mots en géométrie discrète (Attention : 14h)

Abstract: (Hide abstracts)
Les travaux présentés dans cet exposé se situeront au carrefour de la géométrie discrète et de la combinatoire des mots. Je m'intéresserai en particulier aux relations entre ces disciplines et montrerai, comment obtenir de nombreuses propriétés (propriétés structurelles, statistiques...) des plans et surfaces discrets (analogues discrets des plans et des surfaces usuels) à partir d'un codage des ces objets par des mots bidimensionnels indexés par Z2. Je terminerai mon exposé par l'énoncé de quelques perspectives de recherches ainsi que quelques questions ouvertes auxquelles je m'intéresse actuellement.

Thursday 19th January 2006 at 10h Pierre Hyvernat (Institut mathématique de Luminy),
Programmation, simulations, topologie et types dépendants (and much more if time permits)

Abstract: (Hide abstracts)
En partant d'une structure généralisant les graphes de transitions et les simulations, je montrerai comment relier les notions de programmes (ceux de la vraie vie) et de fonctions continues (celles de la topologie constructive). Ceci donne un contenu concret à la 171 topologie formelle 187 de Giovanni Sambin et peut-être vu comme une extension de l'isomorphisme de Curry-Howard. De plus tous les résultats peuvent être développés dans la théorie des types dépendants 171 à la suédoise 187. Plus généralement, la notion utilisée permet de décrire tout phénomène interactif entre un utilisateur et son environnement. La structure résultante permet, entre autre, de donner un modèle non-trivial du lambda-calcul différentiel et semble ainsi relier deux visions des calculs de processus. (??)

Thursday 12th January 2006 at 10h15 Katell Morin-Allory
A proof of correctness for the construction of property monitors

Abstract: (Hide abstracts)
We prove the correctness of an original method for generating components that capture the occurrence of events, and monitor logical and temporal properties of hardware/software embedded systems. The properties are written in PSL, under the form of assertions in declarative form. The method is based on a library of primitive digital components for the PSL temporal operators. These building blocks are interconnected to construct complex properties, resulting in a synthesizable digital module that can be properly linked to the digital system under scrutiny.

Thursday 5th January 2006 at 10h15 Peter Battyanyi
Weak normalization of the Lambda mu calculus with the rules mu' and rho

Abstract: (Hide abstracts)
Le lambda mu calcul symétrique (i.e. le calcul où on a ajouté la règle mu' duale de mu) est fortement normalisable dans le cas typé. Pourtant quand on ajoute la règle rho qui semble n'être qu'une règle de simplification, la forte normalisation est perdue. On garde cependant la faible normalisation. C'est ce qu'on montrera dans cet exposé.

Thursday 8th December 2005 at 10h15 Patrick Thévenon
Typage avec deux flèches

Abstract: (Hide abstracts)
Dans le cadre des grammaires catégorielles abstraites (ACG) introduites par Ph. de Groote, on peut faire des traductions entre différentes structures linguistiques, par exemple syntaxiques et sémantiques. Initialement conçu sur la base du lambda-calcul linéaire utilisé en linguistique, l'expressivité se trouve limitée notamment en sémantique, où l'on souhaiterait utiliser plusieurs fois une même variable. L'idée est alors d'introduire de l'intuitionisme, et donc un lambda-calcul avec deux types de variables et deux types de flèches (intuitionnistes et linéaires). Il est alors naturel de se demander quel peut être le type principal de termes de ce calcul, et quelles sont ses propriétés. Une difficulté provient du fait que lors de la recherche du type principal, des flèches sous-spécifiées peuvent apparaître, qui peuvent indifféremment être remplacées par les flèches linéaires ou des flèches intuitionistes. Pour ne pas compliquer ce lambda-calcul, il serait agréable de trouver des fragments pour lesquels on pourrait donner une notion de type principal sans flèche sous-spécifiée. Dans le cas général nous verrons que c'est impossible, mais que pour deux cas, le cas eta-long et le cas linéaire, nous avons un résultat.

Thursday 8th December 2005 at 10h Stephane Le Roux (ENS Lyon),
Théorie des jeux sans probabilité

Abstract: (Hide abstracts)
Les jeux simultanés sont des objets représentant le scénario informel suivant : des agents effectuent simultanément chacun un choix parmi un ensemble (propre à chaque agent) de choix possibles. En fonction des tous ces choix, on attribue alors un gain à chaque agent. Et c'est tout, le jeux est terminé. Nash a défini une notion d'équilibre dans ces jeux mais il existe des jeux sans équilibre. Si les agents et les choix sont en nombre fini, Nash a montré qu'on pouvait construire d'un jeu une version "probabilisée" qui, elle, possède un équilibre. J'espère montrer lors de ce groupe de travail que l'introduction des probabilités n'était pas la seule solution envisageable. Deux directions possibles sont : 1) Introduire le non déterminisme sans proba. 2) Considérer la structure "la plus générale" dans laquelle on peut définir les équilibres à la Nash et insister sur l'aspect dynamique qui mène à la notion d'équilibre. Dans les deux cas, les concepts sont plus simples que les proba et les équilibres sont calculables. De plus, les ensembles d'équilibres possèdent des propriétés algébriques alors que les équilibres probabilistes sont peu structurés.

Monday 5th December 2005 at 14h Jakub Kozik (Jagiellonian University),
Decidability of density problem for languages

Abstract: (Hide abstracts)
Notion of density is used when there is a need of quantitative considerations on countable sets. It is known fact that it is impossible to construct uniformly distributed probabilistic measure on such set. By now, standard approach to deal with this problem is to consider asymptotic behavior of probabilities in finite subsets of elements of bounded size. The well known results of such approach are 0-1 laws in logic. In the theory of formal languages notion of density was introduced by Berstel. First approaches were focused on regular languages and exploited the theory of formal power series. Natural extension is the notion of conditional density. For any language L let l_n denote number of words of length n in L. Let L,S be languages over finite alphabet such that S is a subset of L. Let p_n denote probability that randomly and uniformly chosen word from L of length not greater than n belongs to S. Language S has conditional density in L if and only if there exists the limit of p_n. Many problems, concerning asymptotic properties of predicate logic formulae with bounded number of variables, can be rephrased in the theory of languages using the above definition. For the classes of grammars C,D the problem of having conditional density is defined as follows: Given two grammats G_L belonging to C and G_S belonging to D, decide whether L(G_S) has conditional density in L(G_L). In my talk I am going to present my result concerning decidability of the problem of conditional density for several classes of grammars.

Thursday 1st December 2005 at 10h15 Christophe Raffalli
Typage sans types, preuve de la préservation du type.

Abstract: (Hide abstracts)
Je donnerai les définitions de bases et la preuve de subject-reduction de mon système.

Thursday 1st December 2005 at 10h Radu Mateescu (INRIA),
Communication mobile à travers des portes immobiles

Abstract: (Hide abstracts)
Les calculs de processus mobiles, tels que le pi-calcul, sont bien adaptés à la description des systèmes distribués comportant des canaux de communication mobiles et des processus qui sont créés/détruits dynamiquement. En revanche, les algèbres de processus classiques, telles que CCS, CSP ou ACP, ne permettent pas une description directe de la mobilité, mais bénéficient d'environnements de simulation et de vérification plus développés. Dans cet exposé, je présenterai une traduction d'un fragment du pi-calcul vers LOTOS et E-LOTOS (des normes ISO issues de CCS et CSP), qui permet de simuler la communication sur des canaux mobiles. Je préciserai également quelques pistes de recherche pour étendre cette traduction vers des fragments plus larges du pi-calcul.

Thursday 24th November 2005 at 10h Claudia Faggian et Patrick Baillot
Meta interactions

Abstract: (Hide abstracts)
Séance informelle sur la ludique ou la complexité implicite ou les relations entre ludique et calculs de processus.

Thursday 17th November 2005 at 10h15 Anne Bouillard (LIP ENS Lyon),
Etude combinatoire et asymptotique du groupe de traces

Abstract: (Hide abstracts)
Un groupe de traces est le quotient d'un groupe libre par des relations de commutation entre certaines lettres. On peut représenter les traces par des tas de pièces colorées. Dans une première partie, nous étudions les groupes de traces d'un point de vue combinatoire et obtenons une formule explicite de la série génératrice d'un groupe de traces, comparable à la formule d'inversion de Möbius pour le monoïde de traces. Dans un deuxième temps, nous utilisons cette formule pour étudier le taux de croissance moyen asymptotique d'un tas de pièces colorées.

Thursday 3rd November 2005 at 10h Christophe Raffalli (LAMA (université de Savoie)),
Typing without types (Types as programs)

Abstract: (Hide abstracts)
We present a new approach to the problem of static typing in languages of the ML family. The basic idea is to generalize the pseudo linear unification algorithm you can use in the Hindley-Milner algorithm. The obtained language is very expressive compared to existing ML implementation and do not require type annotation for many features of ML that usually needs some (like modules, object, ...).

Thursday 13th October 2005 at 14h15 Fairouz Kamareddine (Heriot-Watt University, Edinburgh, Scotland),
Théorie des types

Abstract: (Hide abstracts)
La théorie de types a été inventée au début du 20eme siècle avec le but d'éliminer les paradoxes qui viennent de l'application d'une fonction à elle-même. Le lambda calcul a été développé (par Church) vers 1930 comme une théorie de fonctions. En 1940, Church ajoutait les types à son lambda calcul. Ces types étaient simples, ce qui veut dire qu'ils n'étaient jamais construits par des lieurs (comme un $lambda$). Alors, on a des termes comme $lambda_{x:T}.B$ (qui sont construits par le lieur $lambda$) mais on n'a pas des lieurs qu'on peut utiliser pour construire un type. Malgré l'influence qu'a connue le lambda calcul typé de Church, sa limitation a aboutit a la création de plusieures théories de types dans la deuxième partie du 20eme siècle. Dans ces calculs, les types sont construits par des lieurs. Dans la plupart de ces calculs, on trouve deux lieurs : le $lambda$ (pour construire des termes) et le $Pi$ (ou $forall$, pour construire des types). Ces deux lieurs nous permettent de distinguer les fonctions (qu'on construit avec les $lambda$s) des types (qu'on construit avec les $Pi$). En plus, dans ces calculs, on permet bien la $beta$-réduction mais pas la $Pi$-réduction. Autrement dit, dans ces calculs on a bien la règle : $(lambda_{x:A}.B)C rightarrow B[x:=C]$ Mais pas la règle : $(Pi_{x:A}.B)C rightarrow B[x:=C]$ En particulier, lorsque $b$ a le type $B$, on donne à $(lambda_{x:A}.b)C$ le type $B[x:=C]$ à la place de $(Pi_{x:A}.B)C$. Il y a quelques extensions puissantes des théorie des types qui donnent le même comportement au $Pi$ qu'au $lambda$ (par exemple, en Automath, dans le langage de programmation Henk de Simon Peyton Jones, etc.). Ca nous aboutit à poser la question : pourquoi distinguer entre le $lambda$ et le $Pi$ lorsque des systèmes comme Automath nous montrent qu'il est plus avantageux de traiter les types exactement comme les termes? Dans cette présentation je décrit un système ou les deux lieurs sont identifiés et je montre que ce système a toutes les propriétés qu'on désire d'un système de typage sauf pour l'unicité des types. Mais je démontre aussi que cette perte de l'unicité des types n'est pas grave parce qu'il y a un isomorphisme entre le typage avec deux lieurs et le typage avec un seul lieur et en plus, tous les différent types d'un même terme, suivent le même modèle.

Thursday 22nd September 2005 at 10h Rene Vestergaard (JAIST (Japon)),
Reasoning about Languages with Binding: a first-order foundation and full adequacy

Abstract: (Hide abstracts)
We will look at what is involved in formally proving results about languages with binding. We will in particular focus on what we want to prove, what we actually do prove, and what requirements we need to put on the formalisms that we use.

The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
By year: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018.