Rappel: Séminaire PPS NOW!

Dernier séminaire de la saison!


Le 27/06/2011 07:55, Alexis Saurin a écrit :

Bonjour à tous,

Le séminaire PPS va bientôt s'interrompre pour l'été. Ce jeudi, vous êtes invités à écouter Stéphane Gimenez nous présenter l'avant-dernier séminaire de la saison sous le titre

Reducibility Proof for Normalization of Full Differential Linear Logic

Stéphane Gimenez (PPS)

Jeudi 30 juin à 11h en salle 0C2

Résumé:
Realizability methods allowed to prove normalization results on many typed calculi.  Girard adapted these methods to systems of nets and managed to prove normalization of second order Linear Logic.  Our contribution is to provide an extension of this proof that embrace Full Differential Linear Logic (a logic that can describe both single-use resources and inexhaustible resources).  Anchored within the reducibility framework our proof is modular enough so that further extensions (to second order, to additive constructs or to any other independent feature that can be dealt with using reducibility) come for free.

=======

À NOTER: il y aura café, thé, etc... un quart d'heure avant le début du séminaire: venez un peu en avance!

=======

Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.

Amicalement,

Alexis

Séminaire PPS: Stéphane Gimenez le 30 juin à 11H en 0C2

Bonjour à tous,

Le séminaire PPS va bientôt s'interrompre pour l'été. Ce jeudi, vous êtes invités à écouter Stéphane Gimenez nous présenter l'avant-dernier séminaire de la saison sous le titre

Reducibility Proof for Normalization of Full Differential Linear Logic

Stéphane Gimenez (PPS)

Jeudi 30 juin à 11h en salle 0C2

Résumé:
Realizability methods allowed to prove normalization results on many typed calculi.  Girard adapted these methods to systems of nets and managed to prove normalization of second order Linear Logic.  Our contribution is to provide an extension of this proof that embrace Full Differential Linear Logic (a logic that can describe both single-use resources and inexhaustible resources).  Anchored within the reducibility framework our proof is modular enough so that further extensions (to second order, to additive constructs or to any other independent feature that can be dealt with using reducibility) come for free.

=======

À NOTER: il y aura café, thé, etc... un quart d'heure avant le début du séminaire: venez un peu en avance!

=======

Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.

Amicalement,

Alexis

CORRECTIF Séminaire PPS: Daniel Leivant le **16 juin à 11H** en 0C2

Bonjour à tous,

Une erreur s'est glissée dans l'annonce que je vous avais fait parvenir en fin de semaine dernière: le séminaire de Daniel Leivant aura lieu le 16 juin à 11H en 0C2 et par la même occasion le sujet du séminaire que nous présentera Daniel a également changé; vous le trouverez ci-dessous. Désolé de ce changement.

Alexis

Dynamic logic and its parents

Daniel Leivant (Indiana University & LORIA Nancy)

Résumé: Dynamic logic for imperative programs, and similar deductive formalisms,
can be seen as syntactic sugar for more explicit forms of reasoning, such as first order
theories and second order logic.  This view suggests notions of completeness for dynamic logic, which we argue are more informative and appropriate than the traditional notion of
relative completeness.

=======

À NOTER: il y aura café, thé, etc... un quart d'heure avant le début du séminaire: venez un peu en avance!

=======

Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.

Amicalement,

Alexis

--
Alexis Saurin

Séminaire PPS: Daniel Leivant le 9 juin à 11H en 0C2

de Alexis Saurin alexis.saurin@pps.jussieu.fr à seminaire-pps@pps.jussieu.fr date 23 mai 2011 19:17 objet Séminaire PPS: J. Goubault-Larrecq le 26 mai à 11H en 0C2 envoyé par gmail.com

masquer les détails 23 mai (Il y a 11 jours)

Bonjour à tous,

Nous avons le plaisir d'accueillir Daniel Leivant à la prochaine séance du séminaire PPS du:

Jeudi 9 juin à 11h en salle 0C2

Turing in the sky: machine models for the arithmetical and analytical hierarchies

Daniel Leivant (Indiana University & LORIA Nancy)

Résumé: Alternating Turing machines (ATMs) were invented by Chandra and Stockmeyer (1976) as a generalization of nondeterministic machines. Just like nondeterminstic machines, their interest is not in physical implementation, but as a theoretical tool, since they elegantly bridge time and space. For example, alternating Log-space is PTime, and alternating PTime is Pspace. However, ATMs have not been studied much beyond complexity theory, since any language accepted an ATM is accepted already by a deterministic TM. The underlying reason is that the semantics of ATMs is defined "locally".

We consider a more global semantics for ATMs, which agrees with the tranditional local semantics for time-bounded computations. Surprisingly, our broader semantics has far-reaching consequences: our revised machines accept precisely the inductive (i.e. Pi-1-1) languages, that is the second-order analog of the RE languages.

Alternating deciders, which either accept or reject each input, accept precisely the hyper-elementary (= Delta-1-1) languages. Alternating machines with a uniform bound k on alternations accept precisely level k of the arithmetical hierarchy. Using negation states, with a suitable semantics, ATMs exhaust the entire analytical hierarchy; in fact, the languages accepted by alternating TMs with at most k negation states along any computation trace are precisely the Pi_k^1 languages.

=======

À NOTER: il y aura café, thé, etc... un quart d'heure avant le début du séminaire: venez un peu en avance!

=======

Plus de détails sur le séminaire à http://www.pps.jussieu.fr/seminaire.

Amicalement,

Alexis