3 décembre 2015

Séminaire Chocola à Lyon.

10 décembre 2015, 14:00 : Séminaire

Valentin Blot (university of Bath, CS dept), Typed realizability for first-order classical analysis

We describe a realizability framework for classical first-order logic in which realizers live in (a model of) typed lambda-mu-calculus. This allows a direct interpretation of classical proofs, avoiding the usual negative translation to intuitionistic logic. We prove that (the interpretations of) the usual terms of Gödel's system T realize the axioms of Peano arithmetic, and that under some assumptions on the computational model, the bar recursion operator realizes the axiom of dependent choice. We also perform a proper analysis of relativization, which allows for less technical proofs of adequacy. Extraction of algorithms from proofs of pi-0-2 formulas relies on a novel implementation of Friedman's trick exploiting the control possibilities of the language. This allows to have extracted programs with simpler types than in the case of negative translation followed by intuitionistic realizability.

10 décembre 2015, 10:30 : Séminaire commun MoVe-LDP

Luigi Santocanale (LIF, AMU), Fixed-point elimination in the Intuitionisitic Propositional Calculus

Résumé à venir.

Notez l’horaire inhabituel, et le lieu: quelque part dans le TPR1.

17 décembre 2015

Journée de fin d’année de l’I2M

14 janvier 2016

Séminaire Chocola à Lyon.

11 février 2016

Séminaire Chocola à Lyon.

10 mars 2016

Séminaire Chocola à Lyon.

14 avril 2016

Séminaire Chocola à Lyon.

12 mai 2016

Séminaire Chocola à Lyon.