34 citations · 50 across the 9 of their papers we have counts for
7 papers · 1 filter
Internal Effectful Forcing in System T
Martin H. Escardo, Bruno da Rocha Paiva, Vincent Rahli +1
The effectful forcing technique allows one to show that the denotation of a closed System T term of type in the set-theoretical model is a continuous function $(\m…
The Patch Topology in Univalent Foundations
Igor Arrieta, Martín Hötzel Escardó, Ayberk Tosun
Stone locales together with continuous maps form a coreflective subcategory of spectral locales and perfect maps. A proof in the internal language of an elementary topos was previo…
Parametricity, automorphisms of the universe, and excluded middle
Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine +1
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assumin…
Notions of Anonymous Existence in Martin-Löf Type Theory
Nicolai Kraus, Martín Escardó, Thierry Coquand +1
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedber…
The Herbrand Functional Interpretation of the Double Negation Shift
Martin Escardo, Paulo Oliva
This paper considers a generalisation of selection functions over an arbitrary strong monad , as functionals of type . It is assumed throughout that…
Bar Recursion and Products of Selection Functions
Martin Escardo, Paulo Oliva
We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, f…
Exhaustible sets in higher-type computation
Martin Escardo
We say that a set is exhaustible if it admits algorithmic universal quantification for continuous predicates in finite time, and searchable if there is an algorithm that, given any…