Topology & Informatics days
The slides of talks, which are available, are accessible in the program below
10.15-11.45 Thomas Ehrhard
14-15.30 Christine Tasson
16.15-17.45 Serge Grigorieff
10.15-11.45 Jean Goubault-Larrecq
14-15.30 Achim Jung
16.15-17.45 Jean-Éric Pin
Thursday March 21 and Friday March 22, 2013, from 9h to 17h30.
The goal is to present a few current research topics in theoretical computer science that involve topology in an essential way. There will be 6 one and a half hour talks as well as time for discussion. Each talk will target an audience of mathematicians (who do not necessarily know the informatics involved) and theoretical computer scientists (who do not necessarily know the topology involved). The talks will focus on the following points:
- The informatics background of the topic
- The link with topology
- The topological tools involved
- The results and/or open problems of the area
We want to try to establish a forum for the communities of mathematicians and computer scientists that work in areas with a topological component. This is a short and small-scope pilot meeting to be repeated in expanded form if this has interest.
SPEAKERS, TITLES, and ABSTRACTS
, PPS, Paris 7 and CNRS: Topology in denotational semantics
Starting from theorems of recursion theory, I will first explain why continuity is the basic requirement on morphisms in the denotational semantics of programming languages, as a mathematical account of the fact that a computation, which produces a result is finite. I will describe two models of programming languages: the Scott semantics and the stable semantics and show how they both lead to a logical refinement of functional programming languages: linear logic. Last I will show how, when trying to design denotational models of linear logic based on linear algebra, one is led to introduce topologieswhich are quite different from the Scott topology, but are based on the same intuition that a successful computation is finite. These new models in turn suggest extensions of linear logic.
Jean Goubault-Larrecq, ENS Cachan: On Noetherian spaces and verification
Noetherian spaces were invented in algebraic geometry, with a motivating example that might be the most complicated that one could imagine: the spectrum of a Noetherian ring. I will show how Noetherian spaces arise naturally, and with simpler incarnations, in the context of verification of infinite-state systems. In particular, there is a beautiful connection with the theory of well-quasi-orders (wqo), which Noetherian spaces generalize. And Noetherian spaces led me, with Alain Finkel, to give what I claim is the right generalization of Karp and Miller's covering tree procedure (which applies to Petri nets) to a host of other infinite-state systems.
Now this is the computer science part of the talk.
The mathematical part consists in essentially two tasks: giving alternative, practical characterization of Noetherian spaces (I probably have a dozen or so, which all serve in one way or another), and showing how rich the algebra of Noetherian spaces is. I will at least state, if not prove, the analogues of classical results in wqo theory: e.g., the space of finite words over a Noetherian space is Noetherian (generalizing Higman's Lemma), the space of finite trees over a Noetherian space is Noetherian (generalizing Kruskal's Theorem), the powerset of a Noetherian space is Noetherian (a result without an equivalent in wqo theory).
Serge Grigorieff, LIAFA, Paris 7 and CNRS: Quasi-Polish Spaces and Choquet Games
Quasi-Polish spaces generalize both Polish spaces and countably based continuous domains (a class introduced in computer science by Dana Scott in 1970). They can be seen as the analog of Polish spaces when Hausdorff T2 axiom (topology separates points) is replaced by Kolmogorov T0 axiom (topology distinguishes points). A paradigm of such quasi-Polish spaces is the T0 analog of the Cantor space, namely P(N) endowed with the topology of purely positive information for which a basic open set is the family of subsets of N containing a given finite set. In a fundamental recent paper, Matthew de Brecht showed that a large part of the theory of Polish spaces admits a counterpart with quasi-Polish spaces. In a joint work with Verónica Becher, we introduce a new characterization of quasi-Polish spaces which has the flavor of Scott domains and has also an interpretation in terms of Choquet games.
Achim Jung, University of Birmingham, UK: Kripke semantics for modal bilattice logic
We employ the well-developed and powerful techniques of algebraic semantics and Priestley duality to set up a Kripke semantics for a modal expansion of Arieli and Avron's bilattice logic, itself based on Belnap's four-valued logic. We obtain soundness and completeness of a Hilbert-style derivation system for this logic with respect to four-valued Kripke frames, the standard model in this setting. The proof is via intermediary relational structures which are analysed through a topological reading of one of the axioms of the logic. Both local and global consequence on the models are covered. (This is joint work with Umberto Rivieccio.)
Jean-Éric Pin, LIAFA, Paris 7 and CNRS: Formal languages and Pervin spaces
This lecture is based on a joint work with M. Gehrke and S. Grigorieff (2010) in which topological tools were used to classify formal languages. A lattice of languages is a set of languages closed under finite intersections and finite unions. As any bounded distributive lattice, a lattice of languages has a dual space in Stone-Priestley duality
(I will explain this notion, but for now it suffices to know that it is a compact space). Now the key idea is to study lattices of languages through properties of their dual spaces.
(1) In the first part of the lecture, I will survey the necessary background on formal languages, introduce the notion of a dual space and give a few basic examples.
(2) In the second part, I will focus on the actual computation of a dual space. Several equivalent definitions are possible, but I will focus on the approach using
Pervin spaces. A Pervin space is simply a set equipped with a lattice of subsets. This notion suffices to define a natural notion of completion and the dual of a lattice of languages is now precisely equal to this completion. Further examples and applications will be given.
Complement for topologists.
A Pervin space is a very special case of quasi-uniform space (a notion derived from that of a uniform space by dropping the symmetry axiom). However, the notion of completion is much more problematic for quasi-uniform spaces than for uniform spaces. But for Pervin spaces, this problem not only disappears,but the whole theory becomes even simpler than for uniform spaces.
Christine Tasson, PPS, Paris 7 and CNRS: Taylor expansion, a round-trip between syntax and semantics
In computer science, denotational semantics is frequently used to study properties of programs independently of their syntax. Although it is less known, semantics is also the starting point of creating new programing languages.
We will focus on quantitative semantics that are designed to count how many ways a result can be computed. In this setting, the interpretation of programs can be seen as Taylor series. This property can be transferred into syntax and we will present how the Taylor expansion of lambda-calculus enables the study of resource consumption of programs. To conclude, we will see that the Taylor series property entails a full abstraction result between probabilistic coherent spaces and a functional programing language - the contextual equivalence of programs is characterized by their semantics. (This is joint work with Ehrhard and Pagani.)
The lectures will take place in the Turing Lecture Hall in the Sophie Germain building on the Paris Left Bank site of Université Paris Diderot, 75013 Paris (the access to the building is from Avenue de France. It is the M6A1 (no. 9) building on this map). See also the access page of the PRG de l’Université Paris Diderot campus.
Participation is free but we ask that you register in order to be sure to have a seat and to help us estimate the the number of participants for the coffee breaks. You register by sending a mail, preferably before March 14 to TopInfo@liafa.univ-paris-diderot.fr