LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Hybrid realizability for intuitionistic and classical choice
- Date
- Tuesday, April 18 2017 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.