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.

Séminaire PPS aujourd'hui à 11h: salle 1D23

Bonjour
Le séminaire PPS accueille aujourd'hui Jonathan Hayman (ENS apris & Cambridge Univ). Nous vous attendons dès 10.45 pour le café !

Graphs, rewriting and causality in rule-based models

The Kappa calculus defines how a graph, representing a system of linked agents, can be modified by rules that specify which changes may occur at places that match specific local patterns. Though the calculus has a wide degree of applicability, it has emerged as a natural description of protein-protein interaction systems and pathways in molecular biology.
This work describes and formalises an intuitive graph-based semantics for Kappa that correctly handles subtle side-effects upon deletion of elements of the graph. Central to the work is the use of spans of morphisms to characterize rewriting in the style of single-pushout based rewriting.
The sequential application of rules gives rise to trajectories, some of which may lead to the production of particular patterns of interest. It is then natural to seek to account for their production with a causal history (a pathway). We introduce several notions of trajectory compression, providing a foundation for techniques to reconstruct causal histories at increasing levels of conciseness.
This is joint work with Vincent Danos, Jérôme Feret, Walter Fontana, Russ Harmer, Jean Krivine, Chris Thompson-Walsh and Glynn Winskel.

Prochain séminaire: Jeudi 14 Juin, 11h, salle 1D23– Jonathan Hayman (ENS Paris)

Bonjour

Le prochain séminaire PPS aura lieu jeudi prochain dans la salle 1D23
habituelle, à 11h.
Jonathan Hayman (ENS Paris et Cambridge Univ) nous parlera de causalité
dans un système de réécriture de graphes à sites pour la biologie des
systèmes.

Une collation avec café, thé et croissants sera servie dès 10.45 dans la
même salle.

-----------------------------------------

Graphs, rewriting and causality in rule-based models

The Kappa calculus defines how a graph, representing a system of linked
agents, can be modified by rules that specify which changes may occur at
places that match specific local patterns. Though the calculus has a
wide degree of applicability, it has emerged as a natural description of
protein-protein interaction systems and pathways in molecular biology.
This work describes and formalises an intuitive graph-based semantics
for Kappa that correctly handles subtle side-effects upon deletion of
elements of the graph. Central to the work is the use of spans of
morphisms to characterize rewriting in the style of single-pushout based
rewriting.
The sequential application of rules gives rise to trajectories, some of
which may lead to the production of particular patterns of interest. It
is then natural to seek to account for their production with a causal
history (a pathway). We introduce several notions of trajectory
compression, providing a foundation for techniques to reconstruct causal
histories at increasing levels of conciseness.
This is joint work with Vincent Danos, Jérôme Feret, Walter Fontana,
Russ Harmer, Jean Krivine, Chris Thompson-Walsh and Glynn Winskel.

Le séminaire PPS c'est ce matin 11h!

Bonjour

Nous accueillons aujourd'hui Daniel Leivant (Indiana Univ) qui nous parlera de théorie de systèmes de données.
C'est a 11h dans la salle habituelle 1D23.

Data systems and their intrinsic theories

Given a multi-sorted free algebra A(C) generated by a set C of
constructors, the intrinsic theory for C has as axioms just the closure
conditions of the types of A(C), and their dual (C-induction).  This gets
interesting when we consider equational programs as added axioms.  For
instance, the programs over N that are provably-typed computes exactly the
provably-recursive functions of PA.
We generalize matters from free algebras to *data-systems*, a setting
where inductive and coinductive definitions can be combined at will, and
untyped equational programs can be assigned semantical (= Curry-style)
types.  The intrinsic theory of a data system has closure conditions for
inductive types, with Induction as their dual, and decomposition
conditions for coinductive types, with a suitable notion of Coinduction as
their dual.
We prove a Data-canonicity Theorem, stating that global program-correctness
over all structures, in a Tarskian-semantics sense, is equivalent to
program-correctness in the canonical structure, in the
denotational-semantics sense. We further show that the intrinsic theory
for any non-trivial data-system is mutually interpretable with PA,
regardless of the mix of inductive and coinductive types. We establish a
strong normalization theorem for all intrinsic theories, and consider its
applications.  Finally, we discuss the relation between an intrinsic
theories based on classical vs constructive logic.

Prochain séminaire pps : Daniel Leivant c'est jeudi 7 à 11h

Jeudi 7 Juin, 11h, salle 1D23– Daniel Leivant (Indiana Univ.) 

Data systems and their intrinsic theories

http://www.pps.univ-paris-diderot.fr/seminaire/sem2012/abstracts/Leivant

Jean Krivine

(M) +33 6 16 25 49 45

Séminaire LIAFA/Algorithmes et Complexité : Vendredi 7 Juin, 14h, salle 1E20– Umesh Vazirani (UC Berkeley)

Bonjour,

Dans la même lignée que le précédent séminaire de PPS, il y aura ce vendredi un séminaire quantique au LIAFA.
Merci de contacter Adi Rosen (en copie de ce mail), si vous souhaitez recevoir les futures annonces du séminaire de l'équipe Algorithmes et Complexité du LIAFA.

Frédéric


Date: 2012-06-07/2012-06-07 [14:00]
Auteur: Umesh Vazirani (UC Berkeley)
Titre: Certifiable Quantum Dice
Résumé:
[ The talk will take place at Chevaleret 1E20 ]

Is it possible to certify that the n-bit output of a random number generator is "really
random"? A possible approach to this question is via the theory of algorithmic
randomness due to Kolmogorov, Chaitin and Solomonoff, which identifies
randomness with uncompressibilityby any Turing Machine. Unfortunately this
definition does not result in an efficient test for randomness. Indeed, in the
classical World it seems impossible to provide such a test.
Quantum mechanics allows for a remarkable random number generator: its output is
certifiably random in the sense that if the output passes a simple statistical test,
and there is no information communicated between the two boxes in the
randomness generating device (based, say, on the speed of light limit imposed
by special relativity), then the output is certifiably random. Moreover, the proof
that the output is truly random does not even depend upon the correctness of
quantum mechanics!

Based on joint work with Thomas Vidick.



On May 29, 2012, at 13:28 , Jean Krivine wrote:

> Bonjour
>
> Le prochain séminaire PPS aura lieu jeudi prochain (31 Mai) à 11h en salle 1D23.
> Nous accueillerons Damian Markham (Telecom ParisTech) qui nous parlera Quantum Computing. Nous espérons vous voir nombreux-ses et dès 10.45 pour la collation café/thé/croissants traditionnelle.
>
> ---------------------
>
> Some quantum quirks for information processing
>
> We will briefly review some of the peculiar features of quantum mechanics which give rise to some of the advantages found in quantum information processing, including quantum key distribution, distributed computation, quantum games and blind quantum computation. We will then outline an intuitive link between measurement based quantum computation and phase transitions in many body physics.

Séminaire Damian Markham

C'est maintenant !

Jean Krivine
(M) +33 6 16 25 49 45

Prochain séminaire PPS: Jeudi 31 Mai, 11h, salle 1D23– Damian Markham (Telecom ParisTech)

Bonjour

Le prochain séminaire PPS aura lieu jeudi prochain (31 Mai) à 11h en salle 1D23.
Nous accueillerons Damian Markham (Telecom ParisTech) qui nous parlera Quantum Computing. Nous espérons vous voir nombreux-ses et dès 10.45 pour la collation café/thé/croissants traditionnelle.

---------------------

Some quantum quirks for information processing

We will briefly review some of the peculiar features of quantum mechanics which give rise to some of the advantages found in quantum information processing, including quantum key distribution, distributed computation, quantum games and blind quantum computation. We will then outline an intuitive link between measurement based quantum computation and phase transitions in many body physics. 

RAPPEL: Prochain séminaire PPS, Jeudi 24 Mai, 11h, salle 1D23– Pierre Fraigniaud (LIAFA)

Le prochain séminaire PPS aura lieu Jeudi 24 Mai. Il sera donné par
Pierre Fraigniaud (LIAFA) et sera précédé, comme d'habitude, d'une
petite collation avec café, thé et croissants, servie dès 10h45 (même
salle).

Wait-free computing, and task checkability

This talk will provide an introduction to distributed shared-memory
wait-free computing, including the way computation is captured by a
model from algebraic topology. In essence, a task is wait-free solvable
if and only if there is a simplicial mapping from a subdivision of the
input complex I to the output complex O. The second part of the talk
will deal with task checkability, where, given a task T and a black box
protocol that claims to solve it, a distributed checker tries to find
out whether the result of an execution is correct. We will show that the
AND-checker is bounded to check only projection-closed tasks. For
arbitrary checker, we will exhibit a tight bound on the minimum number
of values to be used by the checker, as a function of the alternation
number of the task T. The latter is defined as the length of the longest
increasing sequence of simplexes in IxO that is alternating between
correct and incorrect computations.

This is a joint work with Sergio Rajsbaum (UNAM, Mexico), and Corentin
Travers (LaBRI, Bordeaux).

Prochain séminaire PPS: Jeudi 24 Mai, 11h, salle 1D23– Pierre Fraigniaud (LIAFA)

Le prochain séminaire PPS aura lieu Jeudi 24 Mai. Il sera donné par
Pierre Fraigniaud (LIAFA) et sera précédé, comme d'habitude, d'une
petite collation avec café, thé et croissants, servie dès 10h45 (même
salle).

Wait-free computing, and task checkability

This talk will provide an introduction to distributed shared-memory
wait-free computing, including the way computation is captured by a
model from algebraic topology. In essence, a task is wait-free solvable
if and only if there is a simplicial mapping from a subdivision of the
input complex I to the output complex O. The second part of the talk
will deal with task checkability, where, given a task T and a black box
protocol that claims to solve it, a distributed checker tries to find
out whether the result of an execution is correct. We will show that the
AND-checker is bounded to check only projection-closed tasks. For
arbitrary checker, we will exhibit a tight bound on the minimum number
of values to be used by the checker, as a function of the alternation
number of the task T. The latter is defined as the length of the longest
increasing sequence of simplexes in IxO that is alternating between
correct and incorrect computations.

This is a joint work with Sergio Rajsbaum (UNAM, Mexico), and Corentin
Travers (LaBRI, Bordeaux).

Séminaire du labo: c'est ce matin !

Bonjour,

Le séminaire du labo aura lieu ce matin en salle 1D23. Café, thé et
croissant dès 10.45, ensuite:
http://www.pps.jussieu.fr/seminaire/sem2012/abstracts/lenglet

A tout de suite

seminaire PPS- 22/3, 11h, salle 1D23, Abrusci: mini-serie sur les dilatateurs

Chers tous,

demain, le jeudi 22 Mars, 11h, salle 1D23

Michele Abrusci (Roma 3)

va nous donner le premier cours d'une mini-serie sur les dilatateurs:

le jeudi 22 Mars, 11h, salle 1D23:  Dilatateurs

le mardi 27 Mars, 10h, salle 5C03: Pi^1_2-logique

A demain

Claudia

seminaire pps aujourd'hui 20 Mars, 11h, salle 5C03, D. Baelde

Chers tous,
un petit rappel que
aujourd'hui 20 Mars a 11h, salle 5C03,
nous accueillons

David Baelde (Copenhagen):

Formal Proofs of Robustness for Watermarking Algorithms

Abstract:
I will present some new results on the security of watermarking schemes against arbitrary attackers, and their full formalization in Coq. This is joint work with P. Courtieu, D. Gross-Amblard and C. Paulin, as part of the ANR project Scalp which focuses on formal proofs of probabilistic algorithms.

Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data.

We present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.

http://www.pps.jussieu.fr/seminaire/sem2012/abstracts/baelde

seminaire PPS: 20/3 D. Baelde, 22/3 M. Abrusci

Chers tous,
la semaine prochaine est riche en seminaires:

le **mardi** 20 Mars a 11h, salle 5C03
nous accueillons

David Baelde (Copenhagen):

Formal Proofs of Robustness for Watermarking Algorithms

http://www.pps.jussieu.fr/seminaire/sem2012/abstracts/baelde

A suivre, une mini-serie en 2 seminaires sur les dilatateurs par

Michele Abrusci (Roma 3):

le jeudi 22 Mars, 11h, salle 1D23: Dilatateurs
le mardi 27 Mars, 11h, salle 5C03: Pi^1_2-logique

seminaire pps, MARDI 13/3, salle 5C03: Thomas Streicher

Chers tous,

cette semaine, le séminaire a lieu demain,
le **mardi** 13 Mars a 11h
en salle salle 5C03

Nous accueillons

Thomas Streicher (DU Darmstadt)

Krivine's Classical Realizabiliy from a Categorical Perspective

After recalling Krivine's classical realizability we introduce the
notion of an abstract Krivine structure (aks) and characterise those
which correspond to Cohen forcing. We further show how every aks can
be turned into a filtered order pca (in the sense of Hofstra and van
Oosten) giving rise to a tripos which induces a Classical
Realizability Topos by the well known tripos-to-topos construction. 
Finally, we  discuss the question what are the functions on N that are 
representable in the Classical Realizability Topos.

http://www.pps.jussieu.fr/seminaire/

A bientot

Claudia

seminaire PPS 8 Mars, 11h salle 1D23 – Olivier Hermant

Chers tous,
jeudi prochain, 8 Mars,
nous accueillons

Olivier Hermant (ISEP)

"From normalization to cut elimination"

https://www.pps.jussieu.fr/seminaire/

Le séminaire est a 11h en salle 1D23,
et sera précédé d'un pot informel avec café et croissants à partir de 10h45. 

A bientot,

Claudia

seminaire pps, 1 mars **10h** , salle 1D23

Chers tous,
petit rappel que demain, jeudi 1 Mars, nous avons une double seance.

Le séminaire debute a 10h (salle 1D23), et
sera précédé d'un pot informel avec café et croissants à partir de 09h45.

Nous accueillerons:

Benoît Valiron (Philadelphia, US) -- 10h
Toward duplication in denotational semantics of quantum computation.

Arthur Charguéraud (Max Planck Institute, Saarbruecken) - 11h20
Characteristic Formulae for the Verification of Imperative Programs

https://www.pps.jussieu.fr/seminaire/

A bientot,

Claudia

seminaire PPS jeudi 1 Mars: Valiron a 10h00, Chargueraud a 11h20, salle 1D23

Chers tous,

jeudi 1 Mars, nous avons une double seance.

Le séminaire debute cette semaine a 10h (salle 1D23), et
sera précédé d'un pot informel avec café et croissants à partir de 09h45.

Nous accueillerons:

Benoît Valiron (Philadelphia, US) -- 10h
Toward duplication in denotational semantics of quantum computation.

Arthur Charguéraud (Max Planck Institute, Saarbruecken) - 11h20
Characteristic Formulae for the Verification of Imperative Programs

https://www.pps.jussieu.fr/seminaire/

A bientot,

Claudia

Seminaire PPS: Margherita Zorzi, jeudi 16/02 11h salle 1D23

Chers tous,

jeudi prochain,  16 fevrier, nous recevons

Margherita Zorzi (LIPN, Paris)

qui nous donnera un expose sur

An introduction to quantum complexity and quantum ICC

https://www.pps.jussieu.fr/seminaire/

Le séminaire est a 11h en salle 1D23,
et sera précédé d'un pot informel avec café et croissants à partir de 10h45. 

A bientot,

Claudia

Please confirm your subscription to "gigi04"

Hello Friend,

We have received your request for a
subscription to a mailing list maintained by
GetResponse email marketing service.

To confirm your subscription, please
click the following link:

EASY 1-CLICK CONFIRMATION:
http://app.getresponse.com/confirm.html?x=a62b&sq=IVXRB&y=B&

You will be able to unsubscribe
or change your details at any time.

If you have received this email in
error and do not intend to join our
list, no further action is required
on your part.

You won't be subscribed to any
list and you won't receive further
information until you confirm your
subscription above.

--
MABBUT

MABBUT PHILIPPE, QUARTIER SAINTE ANNE, ST MICHEL L'OBS, FRANCE 04870, France

Email address: "Friend" seminaire-pps@pps.jussieu.fr
Type of request: import
Timestamp: 2012-01-30 01:47:50
IP address: 79.82.228.152

RAPPEL Seminaire PPS: Marcelo Fiore, à 11h en salle 1D23

Bonjour,

Venez prendre café, thé et croissant a partir de 10h45 en salle 1D23, ensuite nous aurons le plaisir d'entendre:

Marcelo Fiore (Cambridge), en visite a PPS:

Algebraic Foundations for Type Theories

https://www.pps.jussieu.fr/seminaire/

Jean

Seminaire PPS: Marcelo Fiore, jeudi 26/01 11h salle 1D23

Chers tous, le seminaire de jeudi prochain, 26 janvier, est donne par  Marcelo Fiore (Cambridge), en visite a PPS: Algebraic Foundations for Type Theories https://www.pps.jussieu.fr/seminaire/ Le séminaire est a 11h en salle 1D23, et sera précédé d'un pot informel avec café et croissants à partir de 10h45.  A bientot, Claudia

Seminaire PPS: Silvia Crafa, jeudi 19/01 11h salle 1D23

Chers tous, jeudi prochain, 19 janvier, nous accueillerons Silvia Crafa (Padua, Italie) A spectrum of behavioral relations over LTSs on probability distributions https://www.pps.jussieu.fr/seminaire/ Le séminaire est a 11h en salle 1D23, et sera précédé d'un pot informel avec café et croissants à partir de 10h45. A bientot, Claudia A spectrum of behavioral relations over LTSs on probability distributions Abstract: Probabilistic nondeterministic processes are commonly modeled as probabilistic LTSs (PLTSs, a.k.a. probabilistic automata). A number of logical characterizations of the main behavioral relations on PLTSs have been studied. In particular, Parma and Segala define a probabilistic Hennessy-Milner logic interpreted over distributions, whose logical equivalence/preorder when re- stricted to Dirac distributions coincide with standard bisimulation/simulation be- tween the states of a PLTS. This result is here extended by studying the full log- ical equivalence/preorder between distributions in terms of a notion of bisimula- tion/simulation defined on a LTS of probability distributions (DLTS). We show that the standard spectrum of behavioral relations on nonprobabilistic LTSs as well as its logical characterization in terms of Hennessy-Milner logic scales to the probabilistic setting when considering DLTSs. It is joint work with Francesco Ranzato, presented at CONCUR 2011

seminaire pps, le 12 Janvier: Paul Ruet

Bonjour et bonnee annee a tous!

On debute le 2012 avec un seminaire de Paul Ruet:

Jeudi 12 janvier, 11h salle 1D23 – Paul Ruet (PPS)
Cycles locaux et attracteurs dans les réseaux booléens asynchrones

http://www.pps.jussieu.fr/seminaire/

Le seminaire sera précédé d'un pot informel avec café et croissants à partir de 10h45.

A bientot

claudia