Campus Event Calendar
Event Entry
What and Who
A constructive proof of dependent choice in classical arithmetic via memoization
Étienne Miquey
Inria, Nantes
SWS Colloquium
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.
SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 9 May 2019
10:30
90 Minutes
E1 5
029
Saarbrücken
Abstract
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.
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.
Contact
Annika Meiser
93039105
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
111
SWS Space 2 (6312)
passcode not visible
logged in users only
Annika Meiser, 04/30/2019 16:22
Annika Meiser, 04/30/2019 16:05 -- Created document.
Annika Meiser, 04/30/2019 16:05 -- Created document.