Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:A constructive proof of dependent choice in classical arithmetic via memoization
Speaker:Étienne Miquey
coming from:Inria, Nantes
Speakers Bio:I am Étienne Miquey, currently doing a post-doc in the INRIA team Gallinette (in Nantes) where I mainly work with Guillaume

Munch-Maccagnoni. Previously, I was a PhD student under the co-supervision of Hugo Herbelin (in the IRIF laboratory, Paris)
and Alexandre Miquel (in the Mathematical Institute of the Faculty of Engineering of Montevideo). I am mainly interested in the
computational content of proofs through the Curry-Howard correspondence, and especially in classical logic.

Event Type:SWS Colloquium
Visibility:SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Thursday, 9 May 2019
Duration:90 Minutes
Building:E1 5
In 2012, Herbelin developed a calculus (dPAω) in which constructive proofs for the axioms of countable and dependent choices
can be derived via the memoization of choice functions However, the property of normalization (and therefore the one of soundness)
was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent dependent
types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions
of type ℕ→A into streams (a₀,a₁,…)) and of lazy evaluation with sharing (for these coinductive objects). Building on previous
works, we introduce a variant of dPAω presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine
classical realizability we developed to prove the normalization of classical call-by-need. On the other hand, we benefit of dLtp, a
classical sequent calculus with dependent types in which type safety is ensured using delimited continuations together with a
syntactic restriction. By combining the techniques developed in these papers, we manage to define a realizability interpretation
à la Krivine of our calculus that allows us to prove normalization and soundness. This talk will go over the whole process, starting
from Herbelin’s calculus dPAω until the introduction of its sequent calculus counterpart dLPAω that we prove to be sound.
Name(s):Annika Meiser
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Meeting ID:SWS Space 2 (6312)
Tags, Category, Keywords and additional notes
Attachments, File(s):

Annika Meiser/MPI-SWS, 04/30/2019 04:02 PM
Last modified:
Uwe Brahm/MPII/DE, 05/09/2019 07:01 AM
  • Annika Meiser, 04/30/2019 04:22 PM
  • Annika Meiser, 04/30/2019 04:05 PM -- Created document.