Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Hybrid realizability for intuitionistic and classical choice

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Valentin Blot
Le mardi 18 avril 2017 à 11:00
Salle de Conférence (Pavillon des Jardins)
Valentin Blot (Queen Mary University of London)

The axiom of choice is ubiquitous in mathematics, and its computational interpretation is an important step towards certification of a wide range of programs. However, this computational content is highly dependent on whether we work in classical or in intuitionistic logic (with or without the excluded middle). Indeed, while in an intuitionistic setting the axiom of choice can be interpreted with a simple and purely functional program, its interpretation in the classical case requires strong recursion schemes like bar recursion. This complexity does not come as a surprise since the combination of the axiom of choice with classical logic proves the existence of non- computable functions. I will present a hybrid system encompassing both the classical and intuitionistic settings, where both intuitionistic and classical choice are interpreted with their usual respective realizers. This model relies on a notion of polarity on formulas that keeps track of the uses of classical logic in a proof.

À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents