# Seminar

The seminar generally takes places on Tuesday morning. To keep informed you can

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

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

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

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

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

## 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

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

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

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

## 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 (1mm^{3}). 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é.

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

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

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

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

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

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

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

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

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

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

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

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

## A type theory for weak ω-categories

**Eric Finster**(LIX)

Sunday 4 September 2016 at 11:00, room Marcel-Paul Schützenberger

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

## Consensensus asymptotique dans un réseau dynamique

**Bernadette Charron-Bost**(LIX)

Tuesday 3 May 2016 at 11:00, room Emmy Noether

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

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

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

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

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

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

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Tuesday 8 September 2015 at 10:00, room Robin Milner

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Thursday 3 September 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Thursday 3 September 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Assia Mahboubi**(LIX, École Polytechnique)

Wednesday 8 July 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Wednesday 17 June 2015 at 14:00, room Marcel-Paul Schützenberger

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Wednesday 3 June 2015 at 14:00, room Philippe Flajolet

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Wednesday 20 May 2015 at 14:00, room Philippe Flajolet

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

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Friday 3 April 2015 at 10:30, room Marcel-Paul Schützenberger

## An introduction to Homotopy Type Theory

**Éric Finster**(LIX, École Polytechnique)

Tuesday 24 March 2015 at 13:30, room Philippe Flajolet

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

## 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 2015^{1}. If time permits, I might also outline some more technical results from a recent draft^{2}, related to the “fundamental embedding” of any refinement system into the refinement system of presheaves over categories.

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

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

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

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

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

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

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

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