Skip to Main content Skip to Navigation
Conference papers

Gardening with the Pythia A model of continuity in a dependent setting

Martin Baillon 1 Assia Mahboubi 1 Pierre-Marie Pédrot 1
1 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : We generalize to a rich dependent type theory a proof originally developed by Escardó that all System T functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions. The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (N → N) → N is externally continuous.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03510671
Contributor : Martin Baillon Connect in order to contact the contributor
Submitted on : Tuesday, January 4, 2022 - 3:47:45 PM
Last modification on : Friday, January 21, 2022 - 3:20:14 AM

File

gardening_with_the_pythia.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot. Gardening with the Pythia A model of continuity in a dependent setting. Computer Science Logic, Feb 2022, Göttingen, Germany. ⟨10.4230/LIPIcs.CSL.2022.13⟩. ⟨hal-03510671⟩

Share

Metrics

Les métriques sont temporairement indisponibles