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
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
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
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
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
