Logo_UPD_web.jpg                                 image003.png     image005.png     logopps.png

logoFRMPC.gif     ANR.gifFREC

 

Topology & Informatics days

 

flag_english.gif

SLIDES

 

The slides of talks, which are available, are accessible in the program below

 

PROGRAM

 

Thursday

9:45-10:15 coffee

10.15-11.45 Thomas Ehrhard

11.45-12 discussion/questions

 

14-15.30 Christine Tasson

15.30-15.45 discussion/questions

15.45-16.15 coffee

16.15-17.45 Serge Grigorieff

17.45-18 discussion/questions

 

Friday

9:45-10:15 coffee

10.15-11.45 Jean Goubault-Larrecq

11.45-12 discussion/questions

 

14-15.30 Achim Jung

15.30-15.45 discussion/questions

15.45-16.15 coffee

16.15-17.45 Jean-Éric Pin

17.45-18 discussion/questions

 

 DATES            

 

Thursday March 21 and Friday March 22, 2013, from 9h to 17h30.

 

FORMAT

 

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

 

Thomas Ehrhard, 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.)

 

VENUE

 

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.

 

REGISTRATION

 

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

 

ORGANISATION

 

Mai Gehrke, with the help of Sam van Gool and Maria Esteban