Seminar

This page is not updated anymore: the new page is here.

Robin Piedeleu

A diagrammatic axiomatisation of finite-state automata

Robin Piedeleu (University College London)
Wednesday 27 January 2021 at 11:00, online seminar (recording available)

In this talk I will present a fully diagrammatic approach to the theory of finite-state automata, based on reinterpreting their usual state-transition graphs as string diagrams. Moreover, I will give an equational theory that completely axiomatises language equivalence in this new setting. The proposed axiomatisation is finitary— a result which is provably impossible to obtain for the usual one-dimensional syntax of regular expressions.

Maxime Lucas

Abstract rewriting Internalised

Maxime Lucas (Université Sorbonne Paris Nord)
Wednesday 13 January 2021 at 11:00, online seminar (recording available)

There are two historical trends in rewriting theory: “abstract rewriting”, where one rewrites terms, and “algebraic rewriting”, where one rewrites linear combinations of terms. Although the two theories enjoy similar results, there are subtle differences that prevent the development of a unified theory: for example in algebraic rewriting any reflexive relation is both symmetric and transitive. In this talk we present a generic framework to study rewriting in a category C satisfying some suitable hypothesis. In the case C = Set we recover abstract rewriting, while algebraic rewriting corresponds to the case where C is the category of vector spaces. In this framework, we express notions of termination, confluence and local confluence using a notion of rewriting strategy, and prove an analogue of Newman’s Lemma. Finally, we hint at the higher dimensional analogue of this framework, with a view towards homotopy.

Constantin Enea

Specifying and Verifying Consistency Properties

Constantin Enea (IRIF)
Tuesday 17 March 2020 at 11:00, room Philippe Flajolet

Modern software is typically built with specialized concurrent or distributed objects, which encapsulate shared-memory accesses or message-passing protocols into higher-level abstract data types. These objects are designed to behave according to certain consistency criteria like linearizability, eventual or causal consistency. In this talk, I will give an overview of my recent contributions concerning formal reasoning about concurrent or distributed objects, from efficient testing algorithms to algorithmic verification methods. These results give rise to alternative specification frameworks to characterize the intended behaviors of such objects, which complement the existing generic formalizations of linearizability and weak consistency.

Marie Kerjean

Typing differentiable programming

Marie Kerjean (INRIA Gallinette)
Tuesday 25 February 2020 at 14:00, room Claude Shannon

Differentiable programming is a recent research area: its objective is to express differentiation as a modular algorithmic transformation on rich programming languages. It is in particular motivated by the various applications of automatic differentiation in machine learning or formal calculus. In this talk I will present joint work with Pierre-Marie Pédrot, focusing on the typing system used to express differentiation. We will first review a few examples of differetentiable languages recently exhibited in the literature. This allows to identity the linear Dialectica transformation as a reverse automated differentiation transformation on a higher-order lambda-calculus with positive types. Building on the intuitions provided by Dialectica and distribution theory, we construct a lambda-calculus with an internal differentiation operator. This calculus is typed by a type system inspired by Differential Linear Logic. Noticeably, we are able to express backward automatic differentiation as a call-by-name strategy and forward automatic differentiation as a call-by-value strategy.

Roman Kniazev

Topos-theoretic point of view on directed spaces

Roman Kniazev (LIX)
Monday 15 July 2019 at 15:00, room Philippe Flajolet

Topos theory provides a very general framework for the investigation of connections between geometry and logic. For example, given a topological space X, category of sheaves on a category of open sets of X is a Grothendieck topos, whose internal logic can be applied for reasoning. We attempted to adapt the semantical counterpart for directed spaces: we considered a trace space as a base category for a sheaf topos and found some topos-theoretic invariants. Also, we studied the representation of time in a trace space and the additional structure it brings to the topos. Besides that, we will briefly discuss further research directions, such as types of the internal language and transition to a global description (like small/big topos). This is a report based on my internship in the team.

Éric Goubault

Directed topological complexity

Éric Goubault (LIX)
Monday 1 July 2019 at 11:00, room Philippe Flajolet

I will introduce in this talk a variant of topological complexity, that can be applied to help classify directed spaces, and has applications to the study of dynamical systems in the large, such as differential inclusions. Directed topological complexity looks for specific partitions {F1,…,Fn,…} of the set of reachable states of some directed space X, such that there is a continuous section from each of the Fi to the space of directed paths which is right inverse to the end points map. The size of this partition measures the minimal complexity that a motion planning algorithm should have, for controlling such a system. Also, as in the classical case, this sheds an interesting light on a number of directed invariants, and we discuss in particular dicontractibility. We will also show some examples of calculations on directed graphs, a number of higher-dimensional spaces and in particular, directed spheres. This is ongoing work with Aurélien Sagnier and Michael Farber.

Indranil Saha

Developing Autonomous Multi-Robot Systems for Complex Missions

Indranil Saha (IIT Kanpur)
Tuesday 25 June 2019 at 10:00, room Philippe Flajolet

Autonomous multi-robot systems have tremendous potential to be useful in various applications, including search and rescue, surveillance, law enforcement, precision agriculture, and warehouse management. Given a high-level mission specification for a multi-robot system, it is technically challenging to determine the responsibilities of the individual robots and a plan for them to execute their tasks safely in such a way that the mission becomes successful. In this talk, I will present a framework for developing multi-robot systems where the mission specification is provided using a set of linear temporal logic (LTL) properties, and the dynamics of the robots are captured in the form of a set of motion primitives. We formulate the planning problem as an SMT solving problem and use an off-the-shelf SMT solver to generate safe trajectories for the robots. I will discuss various challenges that we face in scaling up our solution to large-scale multi-robot systems and describe how we address some of those challenges. As an extension, I will present how the multi-robot coverage problem can be effectively solved in our framework.

Jérémy Dubut

Categorical approaches to bisimilarity

Jérémy Dubut (National Institute of Informatics, Tokyo)
Thursday 16 May 2019 at 14:00, room Philippe Flajolet

There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebras, another one is open maps. In this talk, I will describe these two approaches, illustrated by the case of labelled transition systems (almost no knowledge in category theory is needed for this part). I will then describe how it is possible to translate one into the other in some cases. From open maps to coalgebras, this was done by Lasota, using multi-sorted transition systems. From coalgebras to open maps, this was done in my joint work with Thorsten Wißmann, Shin-ya Katsumata and Ichiro Hasuo, where we derived path-categories and trace semantics for free for different flavors of categories of coalgebras with non-deterministic branching. I will illustrate those constructions on various concrete examples (tree automata, regular nominal automata, …).

Pierre Vial

Exact measures of evaluation in classical natural deduction

Pierre Vial (IRIF)
Tuesday 19 March 2019 at 14:00, room Philippe Flajolet

The lambda-mu calculus [Parigot 92] is a computational interpretation of classical natural deduction, which extends the lambda-calculus. We first present non-idempotent intersection and union type systems characterizing head, weak and strong normalization in the lambda-mu calculus. The non-idempotent approach [Gardner 94, de Carvalho 07] provides very simple combinatorial arguments –based on decreasing measures of type derivations– to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head, leftmost-outermost and maximal reduction sequences to normal form. Then, building on [Bernadet-Lengrand 13, Accatoli-Kesner-Lengrand 18], we refine these types system to statically obtain the exact measures of the lengths of these three strategies as well as the sizes of the computed normal forms. In contrast to the literature, we define a unique parametrized system, giving rise to optimally factorized proofs, which encapsulates the three evaluation paradigms/notions of normalization. This parametrized approach may be seen as a general methodological contribution to intersection (and union) type theory. The talk will begin with a gentle introduction to intersection type theory, in particular in the non-idempotent case.

Maxime Lucas

Higher dimensional rewriting and homotopy

Maxime Lucas (INRIA et Laboratoire des Sciences du Numérique de Nantes)
Monday 18 March 2019 at 14:00, room Marcel-Paul Schützenberger

Rewriting theory is traditionally used to study the decidability of equality in various objects. In a seminal paper, Squier made a link between a monoid admitting a presentation which is well-behaved from a rewriting point of view (terminating and confluent in particular), and homotopical properties of this monoid. From this stemmed higher dimensional rewriting theory, which consists in a range of techniques aiming to deduce homotopical information on an object using a well-behaved presentation of this object.

In this talk, we give a general presentation of higher dimensional rewriting applied to monoid and other structures (such as algebras, operads, etc.). We show that (strict) cubical omega-categories form a natural setting in which to express the constructions of higher-dimensional rewriting. In particular, we link the good homotopical properties of the Gray tensor product of cubical omega-categories to the algebraic structure of the local branchings.

Jérémy Ledent

A topological model for dynamic epistemic logic

Jérémy Ledent (LIX / Cosynus)
Wednesday 27 February 2019 at 14:00, room Philippe Flajolet

Epistemic logic is the logic of knowledge; it studies what a set of agents know about the world and about each other. The usual model for multi-agent epistemic logic S5 is based on a Kripke frame, which is a graph whose edges are labeled with agents that do not distinguish between two states. We show that this structure is related to the chromatic simplicial complexes that are used in the topological approach to distributed computability. This allows us to view the input, output and protocol complexes as models of epistemic logic, on which we can interpret formulas saying what the processes know about the system. We then extend this duality to the setting of dynamic epistemic logic in order to describe how the epistemic model evolves when communication happens between the agents. By doing so, we are able to prove impossibility results for task solvability, using logical arguments.

Mirco Giacobbe

Refining Template-polyhedra from Counterexamples

Mirco Giacobbe (IST Austria)
Wednesday 20 February 2019 at 14:30, room Marcel-Paul Schützenberger

Template polyhedra generalize intervals and octagons to polyhedra whose facets are normal to arbitrary sets of directions. They are successfully employed by SpaceEx in the reachability analysis of hybrid automata. While previously, the choice of directions has been left to the user, this talk presents a method for the automatic discovery of directions that generalize and eliminate spurious counterexamples. The method applies to linear and nonlinear hybrid automata with constant derivatives, and to hybrid automata with linear ODE. Our experiments demonstrate its efficacy on the time-unbounded reachability of several benchmarks.

Mirco Giacobbe received BSc and MSc from the University of Trento and MSc from RWTH AAchen, in computer Science. Today he is a PhD student in Henziger’s group, at IST Austria. His work focuses on the analysis of timed and hybrid systems and on the application of formal methods in artificial intelligence and systems biology.

Goran Frehse

Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices

Goran Frehse (U2IS)
Wednesday 20 February 2019 at 14:00, room Marcel-Paul Schützenberger

Approximating the set of reachable states of a dynamical system is an algorithmic yet mathematically rigorous way to reason about its safety. Although progress has been made in the development of efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in the industrial setting. While modern linear algebra packages are efficient for matrices with tens of thousands of dimensions, set-based image computations are limited to a few hundred. We propose to decompose reach set computations such that set operations are performed in low dimensions, while matrix operations like exponentiation are carried out in the full dimension. Our method is applicable both in dense- and discrete-time settings. For a set of standard benchmarks, it shows a speed-up of up to two orders of magnitude compared to the respective state-of-the art tools, with only modest losses in accuracy. For the dense-time case, we show an experiment with more than 10.000 variables, roughly two orders of magnitude higher than possible with previous approaches.

Goran Frehse received a Diploma in electrical engineering and information technology from Karlsruhe Institute of Technology and a PhD in computer science from Radboud University Nijmegen. From 2006 to 2018, he was an associate professor at the University Grenoble Alpes, holding a research fellowship (chaire) from 2016. Since 2018, he is an associate professor at ENSTA ParisTech. He is the architect and lead developer of two well-known model checking tools for hybrid and cyber-physical systems, PHAVer and SpaceEx.

Georg Struth

Generalised Kripke Semantics for Concurrent Quantales

Georg Struth (University of Sheffield)
Monday 14 January 2019 at 15:00, room Grace Hopper

I present ongoing work on a new technique for constructing models of concurrent quantales (and concurrent Kleene algebras). It is inspired by modal correspondence theory for substructural logics and the duality between boolean algebras with operators and relational structures. In our case, frame conditions are given by ternary relations. The operations of concurrent quantales arise as binary modalities—in fact as convolution operations—over quantale-valued functions, parametrised by the ternary frames. The main result so far is a correspondence between concurrent quantales and frame conditions. A first example constructs concurrent quantales and Kleene algebras of weighted shuffle languages from word-level concatenations and shuffles. The second one obtains concurrent quantales of graphs (or graph types) by lifting from the operations of complete join and disjoint union on graphs. Concurrent quantales of pomset languages arise as special cases. Similar constructions in separation logic or interval temporal logics illustrate the universality of the approach, if time permits. Joint work with James Cranch, Simon Doherty, Brijesh Dongol and Ian Hayes

Marie Kerjean

Towards a type theory for differential equations

Marie Kerjean (INRIA Nantes)
Wednesday 28 November 2018 at 10:30, room Grace Hopper

Linear Logic (LL) is a resource-aware refinement of intuitionnistic and classical logic, introduced after a study of denotational models of lambda-calculus. Differential Linear Logic (DiLL) spawned from denotational models LL based on vector spaces. While LL enriches logic with tools from algebra, DiLL transports those of differential calculus. In this talk I will explain how we can refine DiLL into a system which solves linear partial differential equations with constant coefficients. This is done via a semantics study of DiLL, with a focus on smooth and classical models, in which the exponential is interpreted as a space of distributions. From this model, we can then understand exponentials as spaces of solutions to differential equations.

Sergio Mover

Verifying Hybrid Systems with Logic-based Model Checking

Sergio Mover (Cosynus/LIX)
Tuesday 16 October 2018 at 10:30, room Gilles Kahn

Hybrid systems can model complex systems that we have to trust (e.g., the landing gear subsystem of on an airplane) and where software interacts with the physical environment. In this seminar, I will mainly focus on an automatic formal verification technique for Hybrid Systems that is based on a reduction to discrete, but still infinite states, transition systems. I will first explain the first-order logic formalism used to represents discrete systems and verification algorithms based on Satisfiability Modulo Theories (SMT). I will then describe the reduction of (subclasses of) hybrid systems to discrete systems and show different applications of the approach. Then, I will briefly switch topic and introduce an ongoing research project, Fixr, where we tackle the problem of exploiting existing “program artifacts” (e.g., source code, execution traces) to build assistive technology (e.g., similar code search, bug finding, automatic bug repair). I will conclude discussing some future research directions.

Thomas Seiller

Dynamique, algèbre, géométrie, et complexité du calcul

Thomas Seiller (CNRS - Université Paris 13)
Friday 28 September 2018 at 10:30, room Philippe Flajolet

Le but de cet exposé est de présenter certains aspects géométriques des programmes et de la complexité algorithmique qui apparaissent lorsque l’on s’essaie à représenter la dynamique de l’execution des programmes. Le cadre formel que je considère, les modèles de graphes d’interaction, est inspiré des modèles de géométrie de l’interaction de Girard et permet de representer les programmes comme des généralisations de systèmes dynamiques. J’expliquerai comment cette approche me mène à étudier certaines relations d’équivalences entre actions de monoides, et comment ceci pourrait mener à de nouvelles techniques de séparation en complexité.

Nicolas Ninin

Topologie dans le Blue Brain Project

Nicolas Ninin (EPFL)
Friday 21 September 2018 at 14:00, room Marcel-Paul Schützenberger

Dans cette présentations nous présenterons les (ou plutot quelques) utilisation de la topologie que nous pratiquons au Blue Brain Project (BBP). Le BBP est un projet visant à construire un modèle numérique de cerveau de rat le plus précis possible . Depuis quelques années nous disposons d’une première version de ceci représentant d’une toute petite partie du néocortex (1mm3). Il est possible de voir ce modèle comme un graphe dirigé et d’appliquer des méthodes de topologie algébrique classique pour tenter de l’analyser. Nous présenterons certains résultats obtenus (en 2015) dans une première partie, puis quelques analyses plus récentes sur des simulations de plasticité.

Krzysztof Ziemianski

Directed paths on cubical complexes

Krzysztof Ziemianski (University of Warsaw)
Monday 28 May 2018 at 15:00, room Marcel-Paul Schützenberger

Let K be a semi-cubical set that satisfies certain mild conditions. I will present a construction of a CW-complex that is homotopy equivalent to the space of directed paths on the geometric realization of K from two fixed vertices of K. This construction satisfies certain minimality condition which makes it useful for direct calculations. Furthermore, this CW-complex carries a “permutahedral” structure - its cells can be identified with products of permutohedra and attaching maps are inclusions of faces. In the case when K is a Euclidean complex this model can be reduced further using Discrete Morse Theory. In some cases, for example if K is the space of states of a PV-program using only one resource, this leads to the optimal construction: the cells of the constructed CW-complex are in 1-1 correspondence with the generators of homology of the directed path space.

Karim Bouyarmane

Planification et contrôle de mouvements corps-complet multi-tâches en robotique humanoïde

Karim Bouyarmane (Université de Lorraine)
Tuesday 6 March 2018 at 10:00, room Grace Hopper

Les robots humanoïdes sont des systèmes robotiques complexes et encore difficiles à contrôler (espace des configurations d’une cinquantaine de dimensions, sous-actionnement de 6 dimensions de cet espace, redondance, systèmes contraints géométriquement par les contacts et les tâches et contraint dynamiquement par l’équilibre statique et/ou dynamique, systèmes hybrides discret-continu par le changement d’état de contact avec l’environnement, nécessité d’intégration d’une base de connaissances importante dans l’interaction avec un environnement pensé par et pour l’humain, etc). Beaucoup de ces problématiques sont soulevées spécifiquement par la nature humanoïde de ces robots, et sont absentes d’autres classes de systèmes robotiques (bras industriels, robots mobiles à roues, drones, robots à pattes quadrupèdes ou hexapodes), ces derniers s’avérant plus efficaces et plus robustes dans l’exécution de tâches spécialisées. Je présenterai un framework complet d’intelligence artificielle de mouvement de ces robots, faisant émerger des comportements et des mouvements quasi-humains à partir d’une base de connaissances minimale. Je présenterai également quelques résultats récents obtenus sur les preuves de complétude, de stabilité, et de convergence des schémas de contrôle temps-réel qui sont proposés et qui constituent les méthodes standard dans l’état de l’art actuel, schémas utilisés notamment dans la plupart des robots du DARPA Robtics Challenge de 2015.

Adina Panchea

Towards autonomous and bio-inspired control system design

Adina Panchea (Cosynus)
Tuesday 16 January 2018 at 14:00, room Philippe Flajolet

In this talk, I will present how I tackled, during my research projects, some of the activities encountered when designing a control system. Designing a control system implies a number of options, decisions and compromises which depend on the properties of the controlled system and on the required performances. To design a control system, the modelling, controller design, analysis, simulation, implementation and verification steps, which represent research directions by themselves, are often required. I applied an alternative old approach of deriving optimal control laws such as inverse problems of variations calculus or inverse optimal control (IOC) which arouse a renewal of interest among researchers during the years. I addressed inverse optimal control and inverse optimization approaches based parametrized Lagrangians, which reduces the nonlinear parametric optimization problems to linear least square optimization, hence being easier to solve. I used IOC approach to analyse and propose simply but efficient bio-inspired models for redundant biological rhythmical motions, such as: arm motion, postural sway-and-balance, fast-and-normal human locomotion and squat movements. Moreover, I used this IOC approach as a tool to discriminate and reproduce the human fast-and-normal gait for patients with Parkinson’s disease (PD). By combining different research topics such as: estimation, least square methods and interval analysis, I propose a novel IOC method solved in a bounded-error framework. Recently, I addressed the navigation planning level for the autonomous navigation of mobile robots and I proposed and validated on an easy to reproduce robotic platform, an optimal (in terms of path length) and robust motion planning algorithm based incremental sampling-based motion algorithm, i.e. Rapidly-exploring Random Tree (RRT) and interval analysis tools.

Aurélien Sagnier

Point de vue de Connes et Consani sur la fonction zêta de Riemann

Aurélien Sagnier (Cosynus)
Tuesday 21 November 2017 at 10:30, room Philippe Flajolet

Nous sommes tous habitués à voir les entiers relatifs comme munis de la structure $(\mathbb{Z},+,\times,\leq)$, i.e., une structure d’anneau ordonné, mais il serait possible de les regarder autrement en « changeant l’ordre » des opérations. Plus précisément on peut munir les entiers de la structure suivante $(\mathbb{Z},\max,+)\circlearrowleft\mathbb{N}^\star$, c’est-à-dire un semi-anneau idemptotent avec une action par multiplication (usuelle) des éléments de $\mathbb{N}^\times$, Connes et Consani ont découvert en 2014 qu’on peut « voir » les entiers munis de la structure précédente avec les yeux de la géométrie algébrique comme un espace dont les points sont reliés aux zéros de la fonction zêta de Riemann or en géométrie algébrique pour certaines variétés définies sur des corps finis, l’analogue de l’hypothèse de Riemann a été démontré. Le but est alors d’essayer de transposer la stratégie de la preuve de la conjecture de Riemann pour les fonction zêta associées aux variétés définies sur des corps finis à la fonction zêta de Riemann.

Jean-Eric Pin

Dual space of a lattice as the completion of a Pervin space

Jean-Eric Pin (IRIF)
Friday 30 June 2017 at 11:00, room TBA

In this survey lecture, I will mainly cover well-known results from a new angle. A Pervin space is simply a set equipped with a lattice of subsets. This notion suffices to define a natural notion of completion which appears to be the dual of the original lattice. One can then show that any lattice of subsets can be described by a set of inequations of the form u≤v, where u and v are elements of its dual space. Applications to formal languages and complexity classes will be given.

Adrien Le Coënt

Control synthesis of nonlinear sampled switched systems using Euler's method

Adrien Le Coënt (ENS Paris-Saclay)
Friday 14 April 2017 at 11:00, room Philippe Flajolet

We propose a symbolic control synthesis method for nonlinear sampled switched systems whose vector fields are one-sided Lipschitz. The main idea is to use an approximate model obtained from the forward Euler method to build a guaranteed control. The benefit of this method is that the error introduced by symbolic modeling is bounded by choosing suitable time and space discretizations. The method is implemented in the interpreted language Octave. Several examples of the literature are performed and the results are compared with results obtained with a previous method based on the Runge-Kutta integration method.

Alexander Kurz

Relation Lifting

Alexander Kurz (University of Leicester)
Monday 27 March 2017 at 15:30, room Marcel-Paul Schützenberger

Going back to work by Barr in the 1970ies, the question of how to extend constructions given in terms of maps to constructions given in terms of relations has received considerable attention. For example, in the semantics of programming languages this question is of fundamental importance if programs are abstracted as maps and specifications as relations. We will review the well-known result characterising liftings of functors from sets and maps to sets and relations and then generalise it from sets to partial orders and to metric spaces. Applications to process algebra, modal logic and domain theory will be discussed. The material presented will be based on the work of, amongst others, Barr, Hermida, Jacobs, Levy, Marti, Venema as well as on joint work with my coauthors Bilkova, Jung, Moshier, Petrisan, Velebil.

Uli Fahrenberg

Semirings, semimodules, and star-continuity

Uli Fahrenberg (LIX)
Wednesday 22 March 2017 at 14:00, room Philippe Flajolet

Semirings are algebraic structures which abound in computer science. Motivated by applications in automata theory, semirings with iteration structures (star semirings, Conway semirings, star-continuous Kleene algebras) have seen extensive development since the 50ies. In order to handle infinite runs, Bloom, Ésik, Kuich and others have developed the algebraic setting of semiring-semimodule pairs with infinite products, with applications in Büchi automata, energy problems and other areas. I will give a gentle introduction to the above algebraic setting, with plenty of motivation and examples. Afterwards, I will give an exposition of recent work on star-continuous Kleene ω-algebras which I have done with the late Zoltán Ésik, including its application to energy problems.

Ignacio Fábregas

When Are Prime Formulae Characteristic?

Ignacio Fábregas (Reykjavik University)
Monday 13 March 2017 at 15:30, room Grace Hopper

In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to the logics characterizing all the semantics in van Glabbeek’s branching-time spectrum.

Jérémy Ledent

A cartesian-closed category for higher-order model checking

Jérémy Ledent (LIX)
Tuesday 28 February 2017 at 10:30, room Philippe Flajolet

In previous work, Martin Hofmann and Wei Chen have described the construction of an abstract lattice from a given Büchi automaton. This abstract lattice is finite and is related by a Galois insertion to the lattice of languages of finite and infinite words. This allows one to decide whether finite and infinite traces of (sequential) non-deterministic first-order recursive programs are accepted by the automaton. In this talk I will show how to extend this work to higher-order programs. This involves the construction of a cartesian-closed category with a fixpoint operator, such that the interpretation of a higher-order recursive program yields precisely the abstraction of its set of finite and infinite traces. This provides an algorithm for the higher-order model checking problem for trace properties by computing the interpretation of a program in this category. It was already known (Ong & Kobayashi) that this higher-order model checking problem is decidable, but all previous algorithms work inherently on tree properties, even when we are only interested in trace properties. This algorithm is considerably simpler since it focuses on trace properties.

Christian Johansen

Sculptures for Higher Dimensional Automata

Christian Johansen (University of Oslo)
Thursday 12 January 2017 at 15:00, room Philippe Flajolet

This talk will explain Higher Dimensional Automata (HDA) model of concurrency emphasising the fact that events/activities have duration. My view of HDAs is more from a CS point of view, than geometrical, and thus I explain how transitions are now first class citizens, the same as nodes are in standard FSM. Finite state machines are the models on which standard modal logics are interpreted, i.e., in states, which contain propositional formulas, whereas the modalities move on transitions from state to state. In comparison, I will present how Higher Dimensional Modal Logic (HDML) is a natural extension of modal logic to consider the transitions as first class citizens and also to consider the concurrency. I will try to explain the attempt at proving the completeness of HDML over HDAs. Difficulty of obtaining the completeness of HDML may be because HDML is close to the ST structures, which are the natural extension of the configuration structures of van Glabbeek and Plotkin by considering the transitions as first class citizens, i.e., the notion of “during” is made explicit. My results suggest that ST structures do not capture all HDAs, but capture only Sculptures. Sculptures are strange, elusive, since they want to capture the intuition given by Pratt about how to build HDAs, but do not capture full HDAs. This brings now the discussion that maybe this is why the completeness of HDML fails. Thus, if we pin point where the sculptures sit wrt. HDAs, we may be able to understand where the completeness fails for HDML. Note that this talk will be given in a manner understandable also for non-experts in HDA or in HDML. Though some familiarity with modal logics or with event-based models of concurrency would help.

Simon Forest

Complexes de parité et pasting schemes

Simon Forest (ENS)
Wednesday 19 October 2016 at 14:00, room Philippe Flajolet

Les ∞-catégories sont une généralisation des catégories où il y a non seulement des morphismes entre objets, mais plus généralement des (n+1)-morphismes entre n-morphismes. Ces catégories généralisées doivent vérifier plusieurs axiomes, notamment l’associativité de la composition ainsi que la loi d’échange. Ces axiomes rendent la représentation de morphismes sous la forme de formules de composition assez maladroite pour plusieurs raisons. D’abord car les formules deviennent rapidement très lourdes et peu intuitives. Mais aussi car les axiomes des ∞-catégories rendent la classe d’équivalence d’une formule difficile à décrire, ce qui en pratique empêche de choisir une formule canonique par morphisme ou de décider facilement de l’égalité de deux formules. Dans ce cadre, Street et Johnson ont introduit des théories permettant de représenter une certaine classe de ∞-catégories à l’aide de structures basées sur des ensembles. Ces structures permettent de représenter chaque morphisme par un élément unique (donc canonique) et fournissent donc une façon plus commode de représenter les morphismes que les formules de composition. Dans cet exposé, on essayera de mieux comprendre ces deux structures et de les comparer. À partir de cette analyse, on donnera une généralisation axiomatiquement plus simple et qui permet de représenter plus de cas.

Eric Finster

A type theory for weak ω-categories

Eric Finster (LIX)
Sunday 4 September 2016 at 11:00, room Marcel-Paul Schützenberger
Shane Mansfield

An Overview of the Sheaf-theoretic Approach to Contextuality

Shane Mansfield (IRIF)
Monday 23 May 2016 at 13:30, room Philippe Flajolet

Contextuality is a key feature which distinguishes super-classical (e.g. quantum) correlations from classical ones. In the quantum setting it is the subject of celebrated no-go theorems of Bell, Kochen-Specker, and others. We will also mention recent results suggesting that it is the essential ingredient for enabling quantum advantages over classical computing in various settings. The language of sheaf theory and algebraic topology provides a powerful, general setting in which to treat contextuality. In this talk we will present an overview of the approach. We will see that empirical data can be represented as a compatible family of sections in a certain presheaf of probability distributions, and that contextuality is characterised by the absence of any global section which recovers the empirical data by restriction. The perspective uncovers a rich hierarchy of qualitatively different levels of contextuality, leads to a cohomological characterisation of certain kinds of contextuality, and to a geometric understanding of empirical models over fixed scenarios which enables quantification of contextuality via simple linear programs.

Bernadette Charron-Bost

Consensensus asymptotique dans un réseau dynamique

Bernadette Charron-Bost (LIX)
Tuesday 3 May 2016 at 11:00, room Emmy Noether
Goran Frehse

Reachability in Space-Time for Piecewise Affine Dynamics

Goran Frehse (Verimag)
Thursday 3 March 2016 at 10:30, room Grace Hopper

In set-based reachability, a cover of the reachable states of a hybrid system is obtained by repeatedly computing one-step successor states. It can be used to show safety or to obtain quantitative information, e.g., for finding bounds on the jitter in an oscillator circuit. In general, one-step successors can only be computed approximately and are difficult to scale in the number of continuous variables. The approximation error requires particular attention since it can accumulate rapidly, leading to a coarse cover, prohibitive state explosion, or preventing termination. We present an approach with precise control over the balance between approximation error and scalability. By lazy evaluation of abstract set representations, the precision can be increased in a targeted manner, e.g., to show that a particular transition is spurious. Each evaluation step scales well in the number of continuous variables. The set representations are particularly suited for clustering and containment checking, which are essential for reducing the state explosion. This provides the building blocks for refining the cover of the reachable set just enough to show a property of interest. The approach is illustrated on several examples.

Sameh Mohamed

A Topological Method for Finding Invariant Sets of Switched Systems

Sameh Mohamed (LIX, École Polytechnique)
Monday 15 February 2016 at 10:30, room Philippe Flajolet

We revisit the problem of finding invariants sets, or more generally speaking, viability kernels, for a class of differential inclusions, using topological methods based on Wazewski property. In many ways, this generalizes the Viability Theorem approach, which is itself a generalization of the Lyapunov function approach for systems described by ordinary differential equations. We give a computable criterion based on SOS methods for a class of differential inclusions to have a non-empty viability kernel within some given region. We use this method to prove the existence of invariant sets of switched systems inside a region described by a polynomial template, both with time-dependent switching and with state-based switching through a finite set of hypersurfaces.

Assalé Adjé

Itérations sur les politiques pour les systèmes affines par morceaux

Assalé Adjé (IRIT)
Tuesday 12 January 2016 at 10:30, room Marcel-Paul Schützenberger

Dans cette présentation, je montrerai comment utiliser la théorie des fonctions de Lyapunov quadratiques par morceaux pour calculer automatiquement des bornes sur les valeurs atteignables d’un système dynamique affine par morceaux à temps discret. Dans un deuxième temps, je développerai une méthode d’itérations sur les politiques pour obtenir une surapproximation plus précise des ensembles des valeurs atteignables.

Ulrich Fahrenberg

Partial Higher-Dimensional Automata, Bisimilarity, and Natural Homology

Ulrich Fahrenberg (IRISA Rennes)
Thursday 26 November 2015 at 10:00, room Philippe Flajolet

We propose a generalization of higher-dimensional automata, partial HDA. Unlike HDA, and also extending event structures and Petri nets, partial HDA can model phenomena such as priorities or the disabling of an event by another event. Using open maps and unfoldings, we introduce a natural notion of (higher-dimensional) bisimilarity for partial HDA and relate it to history-preserving bisimilarity and split bisimilarity. Higher-dimensional bisimilarity has a game characterization and is decidable in polynomial time. We also explore the relationship between bisimilarity of (partial) HDA and bisimilarity in natural homology.

Fabio Zanassi

Interacting Hopf Algebras - an axiomatisation of linear systems

Fabio Zanassi (ENS Lyon)
Monday 23 November 2015 at 14:00, room Philippe Flajolet

We present by generators and equations the theory IH whose free model is the category of linear subspaces over a field k. Terms of IH are string diagrams which, for different choices of k, express different kinds of networks and graphical formalisms used by scientists in various fields, such as categorical quantum mechanics, concurrency and control theory. The equations of IH arise by distributive laws between PROPs of Hopf algebras – from which the name “Interacting Hopf algebras”. The characterisation in terms of subspaces allows to think of IH as a string diagrammatic syntax for linear algebra: linear maps, spaces and their transformations are all faithfully represented in the graphical language, resulting in an alternative, often insightful perspective on the subject matter. As main application, we use IH to axiomatise a formal semantics of signal processing circuits, for which we study full abstraction and realisability. Our analysis suggests a reflection about the role of causality in the semantics of computing devices. This is a joint work with Filippo Bonchi and Pawel Sobocinski.

Jean Goubault-Larrecq

Order-Theoretic, Geometric and Combinatorial Models of Intuitionistic S4 Proofs

Jean Goubault-Larrecq (LSV, ENS Cachan)
Monday 14 September 2015 at 14:00, room Philippe Flajolet

We propose a few models of proof terms for the intuitionistic modal propositional logic S4. Some of them are based on partial orders, or cpos, or dcpos, some of them on a suitable category of topological spaces and continuous maps. A structure that emerges from these interpretations is that of augmented simplicial sets. This leads to so-called combinatorial models, where simplices play an important role: the point is that the simplicial structure interprets the □ modality, and that the category of augmented simplicial sets is itself already a model of intuitionistic propositional S4 proof terms. In fact, this category is an elementary topos, and is therefore a prime candidate to interpret all proof terms for intuitionistic S4 set theory. Finally, we suggest that geometric-like realizations functors provide a recipe to build other models of intuitionistic propositional S4 proof terms.

Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Tuesday 8 September 2015 at 10:00, room Robin Milner
Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Thursday 3 September 2015 at 14:00, room Philippe Flajolet
Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Thursday 3 September 2015 at 14:00, room Philippe Flajolet
Assia Mahboubi

An introduction to Homotopy Type Theory

Assia Mahboubi (LIX, École Polytechnique)
Wednesday 8 July 2015 at 14:00, room Philippe Flajolet
Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Wednesday 17 June 2015 at 14:00, room Marcel-Paul Schützenberger
Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Wednesday 3 June 2015 at 14:00, room Philippe Flajolet
Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Wednesday 20 May 2015 at 14:00, room Philippe Flajolet
Cyril Cohen

A cubical evaluation model for Type Theory

Cyril Cohen (Inria Sophia Antipolis)
Tuesday 21 April 2015 at 10:30, room Philippe Flajolet

The connection between Type Theory and Homotopy Theory as described by Vladimir Voevodsky’s simplicial set model of type theory does not explain the computational behaviour of the univalence axiom. I will introduce cubical sets with connections and explain why they form a model of type theory that we could use to compute with univalence. The talk will consist of chosen bits from Thierry Coquand’s lectures notes. This new type theory has an ongoing implementation in Haskell.

Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Friday 3 April 2015 at 10:30, room Marcel-Paul Schützenberger
Éric Finster

An introduction to Homotopy Type Theory

Éric Finster (LIX, École Polytechnique)
Tuesday 24 March 2015 at 13:30, room Philippe Flajolet
Eva Darulova

Programming with Numerical Uncertainties

Eva Darulova (EPFL)
Monday 23 March 2015 at 13:30, room Marcel-Paul Schützenberger

Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. Finite-precision arithmetic, such as fixed-point or floating-point, is a common and efficient choice, but introduces an uncertainty on the computed result that is often very hard to quantify. We need adequate tools to estimate the errors introduced in order to choose suitable approximations which satisfy the accuracy requirements. I will present a new programming model where the scientist writes his or her numerical program in a real-valued specification language with explicit error annotations. It is then the task of our verifying compiler to select a suitable floating-point or fixed-point data type which guarantees the needed accuracy. I will show how a combination of SMT theorem proving, interval and affine arithmetic and function derivatives yields an accurate, sound and automated error estimation which can handle nonlinearity, discontinuities and certain classes of loops. We have further combined our error computation with genetic programming to not only verify but also improve accuracy. Finally, together with techniques from validated numerics we developed a runtime technique to certify solutions of nonlinear systems of equations, quantifying truncation in addition to roundoff errors.

Noam Zeilberger

Functors are Type Refinement Systems

Noam Zeilberger (Mathematical Components group, MSR-INRIA Joint Centre)
Thursday 12 February 2015 at 14:00, room Philipppe Flajolet

There is a standard dogma about how to read type theory through the lens of category theory, based on the idea of viewing a type system as a category of well-typed terms. In a long-running project with Paul-André Melliès, at some point we realized that it is better to view a type system as a functor from a category of typing derivations to a category of underlying terms, and indeed that this can even serve as a working definition of “type system” (or what we now call a “refinement system”), as being (in the most general case) simply an arbitrary functor.

In the talk I want to motivate and introduce this general framework, which was described in our paper at POPL 20151. If time permits, I might also outline some more technical results from a recent draft2, related to the “fundamental embedding” of any refinement system into the refinement system of presheaves over categories.

Florence Clerc

Presenting Categories Modulo a Rewriting System

Florence Clerc (CEA, LIST / PPS, Université Paris 7)
Thursday 29 January 2015 at 14:00, room Marcel-Paul Schützenberger

Presentations of categories are a well-known algebraic tool to provide descriptions of categories by the means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an equivalence relation (in the spirit of rewriting modulo), which is described by equational generators. When those form a convergent (abstract) rewriting system on objects, there are three very natural constructions that can be used to define the category which is described by the presentation: one is based on restricting to objects which are normal forms, one consists in turning equational generators into identities (i.e. considering a quotient category), and one consists in formally adding inverses to equational generators (i.e. localizing the category). We show that, under suitable assumptions on the presentation, the three constructions coincide, thus generalizing celebrated results on presentations of groups. We illustrate our techniques on a non-trivial example, and hint at a generalization for 2-categories.

Jérémy Dubut

Directed homology

Jérémy Dubut (École Normale Supérieure de Cachan)
Tuesday 9 December 2014 at 10:00, room Philipppe Flajolet

The purpose of directed algebraic topology is to study systems in which we have a notion of direction, order, time, in exploring their geometry. A quite natural use (which historically motivated the field in the 90s) is the study of truly concurrent systems, in particular higher dimension automata, introduced by Pratt in 1991. If the theory of directed homotopy (analogue of classical theory of homotopy in a directed setting) is well developed, it lacks of a satisfactory notion of directed homology. We propose in this talk a candidate matching some criteria: invariance by actions refinement, modularity, precision and computability in a finite, loop-free case.

Amaury Pouly

Computational Complexity of the GPAC

Amaury Pouly (LIX, École Polytechnique)
Tuesday 2 December 2014 at 10:00, room Philipppe Flajolet

In 1941, Claude Shannon introduced a model for the Differential Analyzer, called the General Purpose Analog Computer (GPAC). Originally it was presented as a model based on circuits, where several units performing basic operations (e.g. sums, integration) are interconnected. However, Shannon itself realized that functions computed by a GPAC are nothing more than solutions of a special class of differential equations of the form y’=p(y) where p is a (vector of) polynomial. Analog computer have since been replace by digital counterpart. Nevertheless, once can wonder whether the GPAC could in theory have super-Turing computable power. A few years ago, it was shown that Turing-based paradigm and the GPAC have the same computational power. So, switching to analog computers would not enable us to solve the Halting problem, or any uncomputable exotic thing, but we can nonetheless compute everything a Turing machine does (given enough resources), and a return to analog technology would at least not mean a loss of computational power. However, this result did not shed any light on what happens at a computational complexity level: can an analog computer (GPAC) solve a problem faster (modulo polynomial reductions) than a digital computer (Turing machine)? I will provide some elements which show that some reasonable restrictions of the GPAC are actually equivalent to P (polynomial time) and going even further, that we can show an equivalence with the polynomial of computable analysis. This gives an elegant, analog definition for polynomial time computable functions over real numbers.

Hugh Steele

Double Glueing and Models of Linear Logic

Hugh Steele (LIPN, Université Paris 13)
Thursday 27 November 2014 at 10:00, room Philipppe Flajolet

Many full completeness theorems have been established for fragments of linear logic since the notion was first defined by Samson Abramsky and Radha Jagadeesan in their 1992 paper. For the most part, these results are obtained on a case-by-case basis: the subject of each proof is precisely one category. In this talk it is shown that certain double glueing constructions can transform tensor-generated compact closed categories with finite biproducts into stronger models of linear logic. By creating a “glueing” over homfunctors and using only standard linear algebra, we show that every such category can act as the basis of a fully complete model of unit-free MLL. We also discuss how the category of hypercoherence spaces can also be seen as a double-glued category, and that the associated construction may be generalised to help create a family of accurate unit-free MALL models.

Éric Finster

Opetopic Diagrams as a Language for Higher Categorical Proofs

Éric Finster (EPFL)
Friday 21 November 2014 at 10:00, room Philipppe Flajolet

Recent advances in type theory have demonstrated interesting new links between formal languages, formal proof assistants and ideas from higher category theory. The identity types of Martin-Lof type theory give us a systematic logical formalism for reasoning synthetically about weak infinity groupoids, or equivalently, homotopy types. On the other hand, the problem of applying these ideas to higher categories, in place of higher groupoids, remains open. Here I will demonstrate a prototype proof assistant for higher category theory based on the opetopic model of higher categories. The proof assistant employs a diagrammatic syntax based on the opetopic diagrams of Joyal, Kock, Batanin and Mascari and implements a definition of opetopic higher category due to Thorsten Palm.

Ian Mackie

Linear numeral systems

Ian Mackie (LIX, École Polytechnique)
Tuesday 18 November 2014 at 10:00, room Philipppe Flajolet

We take a fresh look at an old problem of representing natural numbers in the λ-calculus. Our interest is in finding representations where we can compute efficiently (and where possible, in constant time) the following functions: successor, predecessor, addition, subtraction and test for zero. Surprisingly, we find a solution in the linear λ-calculus, where copying and erasing are not permitted.

Thomas Seiller

Cohomological invariants for complexity?

Thomas Seiller (IHES)
Thursday 13 November 2014 at 10:00, room Philipppe Flajolet

This talk will be about recent results at the intersection of complexity theory and logic. In the last decade, several logical systems that characterize complexity classes appeared, some of them defined as variants of Girard’s linear logic – constrained linear logic systems. Studying mathematical models of linear logic and its constrained variants, we can show a correspondance between a hierarchy of complexity classes and a hierarchy of mathematical objects called graphings. This result enables the use of new techniques and invariants, such as cohomological invariants for graphings, in complexity theory.

Jean-Baptiste Jeannin

dTL2: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems

Jean-Baptiste Jeannin (Carnegie Mellon University)
Tuesday 4 November 2014 at 10:00, room Philipppe Flajolet

Differential Dynamic Logic can express important properties about Cyber-Physical Systems, by combining discrete assignments and control structures with differential equations. However it can only express properties about the end state of a system. In this talk, we introduce the differential temporal dynamic logic dTL2, a logic to specify properties about the intermediate states reached by a hybrid system. It combines differential dynamic logic with temporal logic, and supports some linear time temporal properties of LTL. It extends differential temporal dynamic logic dTL with nested temporalities. We provide a semantics and a proof system for the logic dTL2, and show its usefulness for nontrivial temporal properties of hybrid systems. We take particular care to handle the case of alternating universal dynamic and existential temporal modalities and its dual, solving an open problem formulated in previous work.