Zobrazeno 1 - 10
of 142
pro vyhledávání: '"Escardó, Martín"'
Autor:
de Jong, Tom, Escardó, Martín Hötzel
We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setting. That we work predicatively means that we do not assume Voevodsky's
Externí odkaz:
http://arxiv.org/abs/2407.06956
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 previously given by the second-named author. This proof can be easily transl
Externí odkaz:
http://arxiv.org/abs/2402.03134
Autor:
Escardo, Martin
The set-theoretical model of Goedel's system T is not fully abstract. We also briefly discuss fully abstract models of system T.
Externí odkaz:
http://arxiv.org/abs/2303.11075
Autor:
Tosun, Ayberk, Escardó, Martín Hötzel
Publikováno v:
Electronic Notes in Theoretical Informatics and Computer Science, Volume 1 - Proceedings of MFPS XXXVIII (February 22, 2023) entics:10808
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 previously given by the second-named author. This proof can be easily transl
Externí odkaz:
http://arxiv.org/abs/2301.04728
Autor:
Escardó, Martín, Oliva, Paulo
In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type the
Externí odkaz:
http://arxiv.org/abs/2212.07735
Publikováno v:
LIPIcs, volume 269, 2023
The aim of this paper is to refine and extend proposals by Sozeau and Tabareau and by Voevodsky for universe polymorphism in type theory. In those systems judgments can depend on explicit constraints between universe levels. We here present a system
Externí odkaz:
http://arxiv.org/abs/2212.03284
Autor:
de Jong, Tom, Escardó, Martín Hötzel
Publikováno v:
Logical Methods in Computer Science, Volume 19, Issue 2 (May 4, 2023) lmcs:8643
We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on
Externí odkaz:
http://arxiv.org/abs/2111.00482
Autor:
de Jong, Tom, Escardó, Martín Hötzel
We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements e
Externí odkaz:
http://arxiv.org/abs/2102.08812
We give a new syntax independent definition of the notion of a generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. To this end we define inductively how to build a valid signature $
Externí odkaz:
http://arxiv.org/abs/2012.08370
Autor:
de Jong, Tom, Escardó, Martín Hötzel
We develop domain theory in constructive univalent foundations without Voevodsky's resizing axioms. In previous work in this direction, we constructed the Scott model of PCF and proved its computational adequacy, based on directed complete posets (dc
Externí odkaz:
http://arxiv.org/abs/2008.01422