Rappel Séminaire PPS aujourd'hui 8/11 à 11h en salle 1D06 -- café-croissants dès 10H45

Bonjour,

Petit rappel du séminaire de Damien Pous qui débutera à 11H en 1D06 mais vous êtes les bienvenus dès 10H45 autour d'un café.

Les détails sont rappelés ci-dessous.

Alexis

---------- Message transféré ----------
De : Alexis Saurin PPS <alexis.saurin@pps.univ-paris-diderot.fr>
Date : 5 novembre 2012 13:40
Objet : Jeudi 8/11 à 11h en salle 1D06, séance séminaire PPS avec Damien Pous
À : seminaire-pps@pps.jussieu.fr, auliafa@liafa.jussieu.fr


Bonjour,

Comme annoncé lors de la dernière séance du séminaire, nous accueillerons Damien Pous ce jeudi 8 novembre qui viendra nous présenter un article accepté à POPL'13 intitulé Checking NFA equivalence with bisimulations up to congruence (co-écrit avec Filippo Bonchi).

Le séminaire intéressera aussi bien les membres de PPS que ceux du LIAFA.

La séance aura lieu Jeudi 8/11 à 11h en salle 1D06 et nous vous rappelons que café et thé seront servis dès 10h45 dans la salle du séminaire où nous espérons vous voir nombreux.

Checking NFA equivalence with bisimulations up to congruence
Damien Pous (CNRS & ENS-Lyon)
Jeudi 8/11 à 11h en salle 1D06
http://www.pps.univ-paris-diderot.fr/seminaire/sem2012/abstracts/Pous

Résumé: We introduce "bisimulation up to congruence" as a technique for
proving language equivalence of non-deterministic finite automata.
Exploiting this technique, we devise an optimisation of the classical
algorithm by Hopcroft and Karp which, as we show, is exploiting a
weaker "bisimulation up to equivalence" technique. The resulting
algorithm can be exponentially faster than the recently introduced
"antichain algorithms".


Cordialement,
L'équipe du Séminaire

--
Alexis Saurin
Chargé de Recherche CNRS
Laboratoire PPS, UMR 7126
Équipe PiR2
CNRS, Université Paris Diderot et INRIA
alexis.saurin@pps.univ-paris-diderot.fr
http://www.pps.univ-paris-diderot.fr/~saurin

Mettez à jour votre carnet d'adresses: mon adresse email professionnelle change, la nouvelle adresse est maintenant alexis.saurin@pps.univ-paris-diderot.fr

Jeudi 8/11 à 11h en salle 1D06, séance séminaire PPS avec Damien Pous

Bonjour,

Comme annoncé lors de la dernière séance du séminaire, nous accueillerons Damien Pous ce jeudi 8 novembre qui viendra nous présenter un article accepté à POPL'13 intitulé Checking NFA equivalence with bisimulations up to congruence (co-écrit avec Filippo Bonchi).

Le séminaire intéressera aussi bien les membres de PPS que ceux du LIAFA.

La séance aura lieu Jeudi 8/11 à 11h en salle 1D06 et nous vous rappelons que café et thé seront servis dès 10h45 dans la salle du séminaire où nous espérons vous voir nombreux.

Checking NFA equivalence with bisimulations up to congruence
Damien Pous (CNRS & ENS-Lyon)
Jeudi 8/11 à 11h en salle 1D06
http://www.pps.univ-paris-diderot.fr/seminaire/sem2012/abstracts/Pous

Résumé: We introduce "bisimulation up to congruence" as a technique for
proving language equivalence of non-deterministic finite automata.
Exploiting this technique, we devise an optimisation of the classical
algorithm by Hopcroft and Karp which, as we show, is exploiting a
weaker "bisimulation up to equivalence" technique. The resulting
algorithm can be exponentially faster than the recently introduced
"antichain algorithms".


Cordialement,
L'équipe du Séminaire

RAPPEL: Jeudi 25/10 à 11h en salle 1D06, séance inaugurale du séminaire PPS avec Gérard Berry

Bonjour,

La séance inaugurale du séminaire PPS 2012-2013 aura lieu Jeudi 25/10 à
11h en salle 1D06 (attention c'est la nouvelle salle jusqu'au
déménagement !).

Nous aurons le plaisir d'accueillir Gérard Berry (Collège de France) qui
nous parlera de la notion de "temps et d'événements en informatique".

https://www.pps.univ-paris-diderot.fr/seminaire/sem2012/abstracts/Berry

Nous espérons vous y voir nombreux et nombreuses. Nous vous rappelons
que café et thé seront servis dès 10h45 dans la salle du séminaire.

Cordialement,
L'équipe du Séminaire

Jeudi 25/10 à 11h en salle 1D06: séance inaugurale du séminaire PPS avec Gérard Berry

Bonjour,

La séance inaugurale du séminaire PPS 2012-2013 aura lieu Jeudi 25/10 à
11h en salle 1D06 (attention c'est la nouvelle salle jusqu'au
déménagement !).

Nous aurons le plaisir d'accueillir Gérard Berry (Collège de France) qui
nous parlera de la notion de "temps et d'événements en informatique".

https://www.pps.univ-paris-diderot.fr/seminaire/sem2012/abstracts/Berry

Nous espérons vous y voir nombreux et nombreuses. Nous vous rappelons
que café et thé seront servis dès 10h45 dans la salle du séminaire.

Cordialement,
L'équipe du Séminaire

Re: Algorithms and Complexity seminar

Dear all,

I remind you our seminar this Tuesday at 10am by Kazuo Iwama, room 1D06.

Frédéric

On 11 sept. 2012, at 10:02, Frederic Magniez <frederic.magniez@liafa.univ-paris-diderot.fr> wrote:

> Dear all,
>
> The seminar of team Algorithms and Complexity will start this year next Tuesday, September 18th, at 10 am in room 1D06.
> Our first speaker is Kazuo Iwama from Kyoto University, who is visiting us this month.
>
> See you Tuesday,
>
> Frederic
>
> ---
> Title: Parameterized Testability
> Speaker: Kazuo Iwama (Kyoto University)
>
> In graph property testing, given a graph represented by an oracle, wear
> want to test whether the graph satisfies some predetermined property P
> or \epsilon-far from satisfying the property. Roughly speaking, a
> graph is called \epsilon-far from a property if we need to modify an
> \epsilon-fraction of the graph to make it satisfy the property. A
> most important focus in this topic has been on general
> characterizations for (constant-time) testable properties, which have
> obtained much progress in the last decade: For the dense graph model,
> Alon et al. finally obtained a purely combinatorial necessary and
> sufficient condition for P to be testable that is closely related to
> the Szemer\'edi Regularity Lemma. For the bounded-degree graph model,
> due to Benjamini et al., any property is testable if it is
> minor-closed.
>
> In this talk, we are still interested in a general framework of
> testable properties, but our approach is a bit different from the
> qualitative one as above. Rather, we are interested in "parameterized
> properties'' that are quite common in NP optimization problems. A bit
> curiously, this direction has not been so popular in the context of
> property testing. The obvious reason is that the problem becomes less
> interesting in both the dense graph model and the bounded degree
> model. For instance, consider the problem k-Vertex Cover for a
> constant k. In the dense graph model, we want to decide whether a
> graph has a vertex cover of size at most k or we need to remove at
> least \epsilon \times n^2 edges to have the property. It turns out
> that this property is easily testable just by accepting only graphs
> with at most \epsilon \times n^2 edges.
>
> To avoid this triviality, we consider the general graph model with an
> augmentation of random edge sampling capability. It is shown that a
> variety of such problems, including k-Vertex Cover, k-Feedback Vertex
> Set, k-Multicut, k-Path Free and k-Dominating Set, are constant-time
> testable if k is constant. It should be noted that the first four
> problems are fixed parameter tractable (FPT) and it turns out that
> algorithmic techniques for their FPT algorithms (bounded-branching
> tree search, color coding, etc.) are also useful for our
> testers. k-Dominating Set is W[2]-hard, but we can still test the
> property in constant time since the definition of \epsilon-farness
> makes the problem trivial for non-sparse graphs that are the source of
> hardness for the original optimization problem. We also consider
> k-Odd Cycle Transversal, which is another well-known FPT problem, but
> we only give a sublinear-time tester when k is a constant. This is a
> joint work with Yuichi Yoshida.
> --

Algorithms and Complexity seminar

Dear all,

The seminar of team Algorithms and Complexity will start this year next Tuesday, September 18th, at 10 am in room 1D06.
Our first speaker is Kazuo Iwama from Kyoto University, who is visiting us this month.

See you Tuesday,

Frederic

---
Title: Parameterized Testability
Speaker: Kazuo Iwama (Kyoto University)

In graph property testing, given a graph represented by an oracle, we
want to test whether the graph satisfies some predetermined property P
or \epsilon-far from satisfying the property. Roughly speaking, a
graph is called \epsilon-far from a property if we need to modify an
\epsilon-fraction of the graph to make it satisfy the property. A
most important focus in this topic has been on general
characterizations for (constant-time) testable properties, which have
obtained much progress in the last decade: For the dense graph model,
Alon et al. finally obtained a purely combinatorial necessary and
sufficient condition for P to be testable that is closely related to
the Szemer\'edi Regularity Lemma. For the bounded-degree graph model,
due to Benjamini et al., any property is testable if it is
minor-closed.

In this talk, we are still interested in a general framework of
testable properties, but our approach is a bit different from the
qualitative one as above. Rather, we are interested in "parameterized
properties'' that are quite common in NP optimization problems. A bit
curiously, this direction has not been so popular in the context of
property testing. The obvious reason is that the problem becomes less
interesting in both the dense graph model and the bounded degree
model. For instance, consider the problem k-Vertex Cover for a
constant k. In the dense graph model, we want to decide whether a
graph has a vertex cover of size at most k or we need to remove at
least \epsilon \times n^2 edges to have the property. It turns out
that this property is easily testable just by accepting only graphs
with at most \epsilon \times n^2 edges.

To avoid this triviality, we consider the general graph model with an
augmentation of random edge sampling capability. It is shown that a
variety of such problems, including k-Vertex Cover, k-Feedback Vertex
Set, k-Multicut, k-Path Free and k-Dominating Set, are constant-time
testable if k is constant. It should be noted that the first four
problems are fixed parameter tractable (FPT) and it turns out that
algorithmic techniques for their FPT algorithms (bounded-branching
tree search, color coding, etc.) are also useful for our
testers. k-Dominating Set is W[2]-hard, but we can still test the
property in constant time since the definition of \epsilon-farness
makes the problem trivial for non-sparse graphs that are the source of
hardness for the original optimization problem. We also consider
k-Odd Cycle Transversal, which is another well-known FPT problem, but
we only give a sublinear-time tester when k is a constant. This is a
joint work with Yuichi Yoshida.
--

Rappel: seminaire PPS aujourd'hui a 11h

Bonjour
Nous accueillons aujourd'hui Jorge Perez (Lisbon Univ.) qui nous parlera des ses travaux présentés a ESOP'12.
La salle (habituelle) c'est 1D23 et l'heure c'est 11h !

A toute a l'heure

Linear Logical Relations and Observational Equivalences for Session-Based Concurrency
(based on an ESOP'12 paper with Luís Caires, Frank Pfenning, and Bernardo Toninho)


In a prior work, Caires and Pfenning proposed an interpretation of intuitionistic linear logic propositions as session types for concurrent processes. The type system obtained from the interpretation ensures fundamental properties of session-based typed disciplines—most notably, type preservation, session fidelity, and global progress.
In this talk, I will present recent developments that complement and strengthen this interpretation. A first development is a theory of logical relations which is based on, and is remarkably similar to, that for functional languages, extended to an (intuitionistic) linear type structure. A main result is that well-typed processes always terminate (strong normalization). A second development is a notion of observational equivalence for session-typed processes. As applications, we prove that all proof conversions induced by the logic interpretation actually express observational equivalences, and explain how type isomorphisms resulting from linear logic equivalences are realized by coercions between interface types of session-based concurrent systems.