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.
jeudi 21 juin 2012
jeudi 14 juin 2012
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.
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.
lundi 11 juin 2012
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 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.
jeudi 7 juin 2012
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.
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.
mercredi 6 juin 2012
Prochain séminaire pps : Daniel Leivant c'est jeudi 7 à 11h
Jeudi 7 Juin, 11h, salle 1D23– Daniel Leivant (Indiana Univ.)
Jean Krivine
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.
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.
Inscription à :
Articles (Atom)