Topology & Informatics days
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