seminaire PPS *MARDI* 31 Mars

Chers tous,
je rappelle (et confirme) le seminaire de demain.

Mardi 31 mars 2009
11h00, Salle 6C1:

Richard Blute (Ottawa)

Introduction to Convenient Vector Spaces

Abstract: We review the basic ideas behind the theory
of smooth spaces and convenient vector spaces, due
to Frolicher and Kriegl. The category of smooth spaces is
a cartesian closed category which naturally contains all
manifolds. Convenient vector spaces are internal vector
spaces in this category. The category is convenient in
that a number of different notions from functional analysis
are combined in this setting. The category also forms a symmetric
monoidal closed category with a comonad making the category a model of
intuitionistic linear logic.

Our hope is that this category will also be a model
of differential linear logic in the sense of Ehrhard and Regnier.

seminaire PPS ***MARDI*** 31 Mars

Chers tous,
le prochaine seminaire PPS est (exceptionelment)
le MARDI.

Mardi 31 mars 2009
11h00, Salle 6C1:

Richard Blute (Ottawa)

Introduction to Convenient Vector Spaces

Abstract: We review the basic ideas behind the theory
of smooth spaces and convenient vector spaces, due
to Frolicher and Kriegl. The category of smooth spaces is
a cartesian closed category which naturally contains all
manifolds. Convenient vector spaces are internal vector
spaces in this category. The category is convenient in
that a number of different notions from functional analysis
are combined in this setting. The category also forms a symmetric
monoidal closed category with a comonad making the category a model
of intuitionistic linear logic.

Our hope is that this category will also be a model
of differential linear logic in the sense of Ehrhard and Regnier.

GdT Semantique 24/3

Bonjour à tous,
le prochain exposé,
le mardi 24 mars 2009
11h00, Salle 6C1:

Giovanni Sambin (Padova)

The notion of stream in constructive topology

The notion of stream, familiar to computer scientists, seems to coincide with
that of choice sequence, introduced by Brouwer in his intuitionistic
reconstruction of the continuum. The streams with entries in a set S are
identified with formal points of a suitable pointfree topology inductively
defined on the set of lists over S. By using a minimalist constructive
foundation, in which not even the so-called axiom of unique choice is valid,
one can have a genuine notion of stream, since one can keep a proper
distinction between streams and sequences which follow some predetermined
instructions (lawlike). This seems impossible in most other foundations.

The inductive generation of formal open subsets is accompanied by its dual, a
coinductive generation of formal closed subsets. A formal closed seems to be
the same as a spread, a notion introduced by Brouwer long ago to specify
some
restrictions on choice sequences. It turns out that a spread being
inhabited by
a stream is a specific example of an important topological property, called
reducibility. It is connected with satisfiability of a condition, and it
is the
dual of spatiality, which is connected with completeness (both in a
logical and
topological sense).

seminaire PPS - 5 Mars

Chers tous,
le prochaine seminaire PPS est donne' par

Ralf Treinen

le Jeudi 5 Mars, 11h, salle 0C2:

Mancoosi: research topics in component-based software

Free and Open Source Software distributions are a particularly interesting
instance of component-based software, due to their distributed development
mode, their importance for today's computing infrastructure, and to their
size. Both the construction of a coherent collection of components, and
the maintenance of software installations based on these, raise difficult
problems for distribution editors and system administrators: Distributions
evolve rapidly by integrating new versions of software packages that are
independently developed. System upgrades may proceed on different paths
depending on the current state of a system and the available software
packages, and system administrators are faced with choices of upgrade
paths, and possibly with failing upgrades.

The ongoing Mancoosi project (Managing the Complexity of the Open Source
Infrastructure) aims to solve some of these problems. In this talk we will
describe past and ongoing work in the context of Mancoosi and its
predecessor project EDOS, as well as some possible future research
directions.