[Séminaire PPS] 10/12 A. Schmitt

Séminaire PPS

175 rue du Chevaleret, Paris 13ème.

Jeudi 10 Décembre, 11h salle 0D1 – Alan Schmitt (INRIA Grenoble),
[attention à la salle !]
Expressivity in higher order calculi

[Seminaire PPS] L. Vaux 3/12

Séminaire PPS

175 rue du Chevaleret, Paris 13ème.

Jeudi 3 Décembre, 11h salle 3E91 – Lionel Vaux (U. Marseille),
Points fixes et types de données dans le modèle relationnel finitaire



---------------
A suivre :

Jeudi 10 Décembre, 11h salle 3E91 – Alan Schmitt (INRIA Grenoble),
Expressivity in higher order calculi

Jeudi 17 Décembre, 11h salle 3E91 – Christian Retoré (U. Bordeaux),
TBA
----------------

[Seminaire PPS]: 26/11 Antoine Miné

Séminaire PPS

175 rue du Chevaleret, Paris 13ème.

Jeudi 26 Novembre, 11h salle 3E91 – Antoine Miné (ENS, Paris),
Static analysis of run-time errors in parallel embedded C code

[Seminaire PPS] 19/11 Pablo Arrighi

Séminaire PPS

175 rue du Chevaleret, Paris 13ème.

Jeudi 19 Novembre, 11h salle 3E91 – Pablo Arrighi (U. Grenoble),

A System F accounting for scalars

[Seminaire PPS] 15/10: Andreas Abel

Séminaire PPS

175 rue du Chevaleret, Paris 13ème.

Jeudi 15 Octobre, 11h, salle 3E91 -- Andreas Abel (LMU, Munich),
Normalization by Evaluation for Dependent Type Theory
<https://www.pps.jussieu.fr/seminaire/sem2009/abstracts/abel>

[Seminaire PPS] H. Herbelin 24/09

Séminaire PPS

Jeudi à 11h,
175 rue du Chevaleret, Paris 13ème.

Jeudi 24 Septembre, salle 3E91 -- Hugo Herbelin (INRIA et PPS),
Sur quelques problèmes ouverts de la théorie de Coq et leurs conséquences pratiques

A suivre:
Jeudi 15 Octobre, salle 3E91 -- Andreas Abel (LMU, Munich), TBA

seminaire PPS Jeudi 2/7

Chers tous,
le prochaine seminaire PPS est

le Jeudi 2 Juillet,
11h, salle 0C2:

Naohiko Hoshino (RIMS, Kyoto)

Title
Linearization of realizability

Abstract
For every PCA (partial combinatory algebra), we can construct
categories such as effective toposes, assemblies and PERs
(partial equivalence relations). They provide models of
polymorphic lambda calculus and dependent type theory.
In this talk, we consider linearlization of constructions
of these categories. Instead of PCA, we consider an algebra
that is a slight generalization of Abramsky's linear combinatory
algebra (LCA) and observe that construction of assembiles
and PER works well. On the other hand, it appears that
the linearization of the construction of an effective topos
from a tripos, called the Set(p) construction, does not work.

seminaire PPS Jeudi 25/6

Chers tous,
le prochaine seminaire PPS est

Jeudi 25 Juin, 11h, salle 0C2:

Colin Riba (ENS Lyon)

On the Values of Reducibility Candidates

Abstract:
The straightforward elimination of union types is known to break
subject reduction, and for some extensions of the lambda-calculus, to
break strong normalization as well. Similarly, the straightforward
elimination of implicit existential types breaks subject reduction.

We propose elimination rules for union types and implicit existential
quantification which use a form call-by-value issued from Girard's
reducibility candidates. We show that these rules remedy the above
mentioned difficulties,
for strong normalization and, for the existential quantification, for
subject reduction as well.

seminaire PPS Jeudi 11/6

Chers tous,
le prochaine seminaire PPS est

Jeudi 11 Juin,
11h, salle 0C2:

Lorenzo Tortora de Falco (Roma)
Sémantique relationnelle et temps d'exécution en Logique Linéaire

Qu'est-ce qu'un calcul correct ? Une tentative de répondre à la question
est de donner un maximum de place aux calculs non corrects. On sera alors
amené à identifier des propriétés cruciales du calcul, qui seront les
témoins de sa correction (terminaison faible ou forte, confluence,
exécution en temps borné, etc...). En guise d'introduction, je discuterai
du point de vue de la logique linéaire (LL) sur la question, pour prendre
ensuite celui de la sémantique relationnelle sur lequel portera
l'essentiel de l'exposé. Je présenterai les résultats principaux d'un
travail en collaboration avec Daniel De Carvalho et Michele Pagani: 1) un
réseau de preuve de LL est normalisable ssi son interprétation
``exhaustive'' est non vide 2) à partir de l'interprétation de deux
réseaux sans coupures de LL on peut calculer le nombre exact d'étapes
d'élimination des coupures conduisant du réseau obtenu en coupant entre
eux les deux réseaux de départ et sa forme normale. Si le temps le permet,
je discuterai d'une possible amélioration de ce dernier résultat (travail
en cours avec Daniel De Carvalho).

Rappel: seminaire PPS aujourd'hui, Jeudi 7 Mai

Chers tous,
le seminaire PPS aujourd'hui

Jeudi 7 Mai,
11h, salle 0C2:

Harry Mairson (Boston)
Linear Logic and the Complexity of Control Flow Analysis

ABSTRACT
Static program analysis is about predicting the future: it's what
compilers do at compile-time to predict and optimize what happens at
run-time. What is the tradeoff between the efficiency and the precision of
the computed prediction? Control flow analysis (CFA) is a canonical form
of program analysis that answers questions like "can call site X ever call
procedure P?" or "can procedure P ever be called with argument A?" Such
questions can be answered exactly by Girard's geometry of interaction
(GoI), but in the interest of efficiency and time-bounded computation,
control flow analysis computes a crude approximation to GoI, possibly
including false positives.

Different versions of CFA are parameterized by their sensitivity to
calling contexts, as represented by a contour---a sequence of k labels
representing these contexts, analogous to Lévy's labelled lambda calculus.
CFA with larger contours is designed to make the approximation more
precise. A naive calculation shows that 0CFA (i.e., with k=0) can be
solved in polynomial time, and kCFA (k>0, a constant) can be solved in
exponential time. We show that these bounds are exact: the decision
problem for 0CFA is PTIME-hard, and for kCFA is EXPTIME-hard. Each proof
depends on fundamental insights about the linearity of programs. In both
the linear and nonlinear case, contrasting simulations of the linear logic
exponential are used in the analysis. The key idea is to take the
approximation mechanism inherent in CFA, and exploit its crudeness to do
real computation.

This is joint work with David Van Horn (Brandeis University), presented at
the 2008 ACM International Conference on Functional Programming.

seminaire PPS Jeudi 7 Mai

Chers tous,
le prochaine seminaire PPS est

Jeudi 7 Mai,
11h, salle 0C2:

Harry Mairson (Boston)
Linear Logic and the Complexity of Control Flow Analysis

ABSTRACT
Static program analysis is about predicting the future: it's what
compilers do at compile-time to predict and optimize what happens at
run-time. What is the tradeoff between the efficiency and the precision of
the computed prediction? Control flow analysis (CFA) is a canonical form
of program analysis that answers questions like "can call site X ever call
procedure P?" or "can procedure P ever be called with argument A?" Such
questions can be answered exactly by Girard's geometry of interaction
(GoI), but in the interest of efficiency and time-bounded computation,
control flow analysis computes a crude approximation to GoI, possibly
including false positives.

Different versions of CFA are parameterized by their sensitivity to
calling contexts, as represented by a contour---a sequence of k labels
representing these contexts, analogous to Lévy's labelled lambda calculus.
CFA with larger contours is designed to make the approximation more
precise. A naive calculation shows that 0CFA (i.e., with k=0) can be
solved in polynomial time, and kCFA (k>0, a constant) can be solved in
exponential time. We show that these bounds are exact: the decision
problem for 0CFA is PTIME-hard, and for kCFA is EXPTIME-hard. Each proof
depends on fundamental insights about the linearity of programs. In both
the linear and nonlinear case, contrasting simulations of the linear logic
exponential are used in the analysis. The key idea is to take the
approximation mechanism inherent in CFA, and exploit its crudeness to do
real computation.

This is joint work with David Van Horn (Brandeis University), presented at
the 2008 ACM International Conference on Functional Programming.

seminaire PPS Jeudi 9 Avril

Chers tous,
le prochaine seminaire PPS est
Jeudi 9 Avril,
11h, salle 0C2:

Bartek Klin (Cambridge),

Observable monoidal reactive systems

How can one observe a system whose dynamics is defined by a structural
congruence on process terms and a set of reaction rules? In a strong
testing scenario, one's powers are: - to put a system in a known context,
and - to observe that a reaction step has happened. In a weak scenario,
one would want to waive the latter capability, which unfortunately leaves
no possibility to observe anything about the tested system at all.

For the pi-calculus, Honda and Yoshida solved this problem by considering
the notion of insensitive systems and maximal consistent theories. I shall
argue that this solution does not work for reactive systems in general,
and that one should instead look for observation clues in an internal
structure hidden in reaction rules.

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.

seminaire PPS - 26 (oui 26!!) Fevrier

Desolee... petit erreur de date!!
Donc:

Matthieu Sozeau (LRI, Orsay)
le Jeudi 26 Février, 11h, salle 0C2:

"Programming with Dependent Types in Coq"

Coq is a mature proof assistant based on a dependent type theory. However,
while the use of dependent types is the very basis of all the proofs that
are developed in the system, it still requires considerable expertise to
tame their full power when programming. We present a solution to alleviate
this problem as an additional layer on top of the core type theory that
eases programming with strong specifications. We develop a new language
inspired by PVS that allows to separate algorithmic and correctness
concerns when developing programs with rich types, generating proof
obligations on the side in a standard way. We also demonstrate the Program
extension to Coq that implements this method on a non-trivial example:
Finger Trees. We develop an indexed version of this data structure from
which we can derive correct-by-construction priority queues or ropes. This
development also illustrates a recently implemented type class extension
to Coq.

seminaire PPS - 19 Fevrier

Chers tous,
le prochaine seminaire PPS est donne' par

Matthieu Sozeau (LRI, Orsay)
le Jeudi 19 Février, 11h, salle 0C2:

"Programming with Dependent Types in Coq"

Coq is a mature proof assistant based on a dependent type theory. However,
while the use of dependent types is the very basis of all the proofs that
are developed in the system, it still requires considerable expertise to
tame their full power when programming. We present a solution to alleviate
this problem as an additional layer on top of the core type theory that
eases programming with strong specifications. We develop a new language
inspired by PVS that allows to separate algorithmic and correctness
concerns when developing programs with rich types, generating proof
obligations on the side in a standard way. We also demonstrate the Program
extension to Coq that implements this method on a non-trivial example:
Finger Trees. We develop an indexed version of this data structure from
which we can derive correct-by-construction priority queues or ropes. This
development also illustrates a recently implemented type class extension
to Coq.

REPORT seminaire PPS du 19 Fevrier

Chers tous,
donne que jeudi c'est journée nationale de manifestations,
le seminaire du 19/2 par Matthieu Sozeau
est reporte à la semaine prochaine, le Jeudi 26 Février, salle 0C2, 11h.

claudia

> Bonjour,
> le prochaine seminaire PPS sera donné par
>
> Matthieu Sozeau (LRI, Orsay)
> le Jeudi 19 Février, salle 0C2:
>
> "Programming with Dependent Types in Coq"
> ------------------------------------------------
>
> 19/2 Matthieu Sozeau (LRI Orsay)
> Programming with Dependent Types in Coq
>
> Coq is a mature proof assistant based on a dependent type theory. However,
> while the use of dependent types is the very basis of all the proofs that
> are developed in the system, it still requires considerable expertise to
> tame their full power when programming. We present a solution to alleviate
> this problem as an additional layer on top of the core type theory that
> eases programming with strong specifications. We develop a new language
> inspired by PVS that allows to separate algorithmic and correctness
> concerns when developing programs with rich types, generating proof
> obligations on the side in a standard way. We also demonstrate the Program
> extension to Coq that implements this method on a non-trivial example:
> Finger Trees. We develop an indexed version of this data structure from
> which we can derive correct-by-construction priority queues or ropes. This
> development also illustrates a recently implemented type class extension
> to Coq.
>

seminaire PPS - 19 Fevrier

Bonjour,
le prochaine seminaire PPS sera donné par

Matthieu Sozeau (LRI, Orsay)
le Jeudi 19 Février, salle 0C2:

"Programming with Dependent Types in Coq"
------------------------------------------------

19/2 Matthieu Sozeau (LRI Orsay)
Programming with Dependent Types in Coq

Coq is a mature proof assistant based on a dependent type theory. However,
while the use of dependent types is the very basis of all the proofs that
are developed in the system, it still requires considerable expertise to
tame their full power when programming. We present a solution to alleviate
this problem as an additional layer on top of the core type theory that
eases programming with strong specifications. We develop a new language
inspired by PVS that allows to separate algorithmic and correctness
concerns when developing programs with rich types, generating proof
obligations on the side in a standard way. We also demonstrate the Program
extension to Coq that implements this method on a non-trivial example:
Finger Trees. We develop an indexed version of this data structure from
which we can derive correct-by-construction priority queues or ropes. This
development also illustrates a recently implemented type class extension
to Coq.

seminaire PPS - 22/1

Jeudi 22 Janvier, salle 0C2, 11h — Cosimo Laneve (Univ. Bologna),
Reachability analysis in the k-family

The $\Kappa$-calculus is a formalism for modelling molecular
biology where molecules
are terms with internal states and with sites, bonds are represented
by shared names labelling sites, and reactions are represented by
rewriting rules. Depending on the shape of the rewrite rules, several
dialects of the calculus can be obtained. We analyze the
expressive power of some of these dialects by focusing on the thin
boundary between decidability and undecidabiity for problems like
reachability and coverability. This analysis is a first step towards
the design of algorithms for the qualitative analysis of languages
of the $\Kappa$-family.

seminaire PPS - 15/1

SEMINAIRE PPS (http://www.pps.jussieu.fr/seminaire)

Jeudi 15 Janvier, salle 0C2 -- Emmanuel Beffara (IML, Marseille)

Calculs de processus algébriques

Dans cet exposé, je montrerai ce qui se passe quand on ajoute aux
calculs de processus une somme formelle pour laquelle la composition
parallèle est bilinéaire. Le point important est de comprendre ce que
signifie zéro: il s'agit d'un symbole de test (ou d'une exception) et il
permet de décomposer les constructions habituelles du calcul d'une façon
nouvelle et intéressante. De ces remarques, on tire un système de
réécriture confluent sur les processus (et normalisant en l'absence de
réplication) qui permet de décider l'équivalence observationnelle de
processus finis. Les amateurs de lambda-calcul différentiel seront ravis
d'apprendre que la somme formelle correspond entre les deux calculs, de
même que la réduction, dans une certaine mesure.

----------------------------------------
EXPOSES A SUIVRE

Jeudi 22 Janvier, salle 0C2 -- Cosimo Laneve (Univ. Bologna),
Reachability analysis in the k-family

Jeudi 19 Février, salle 0C2 -- Ralf Treinen (PPS, Paris),
TBA

Jeudi 12 Mars, salle 0C2 -- Giuseppe Castagna (PPS, Paris),
TBA