Related papers: Domain Theory in Constructive and Predicative Univ…
We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive…
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…
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…
We develop locale theory constructively and predicatively in univalent foundations (UF), with a particular focus on the theory of spectral and Stone locales. In the context of UF, predicativity refers specifically to the development of…
We develop a constructive theory of continuous domains from the perspective of program extraction. Our goal that programs represent (provably correct) computation without witnesses of correctness is achieved by formulating correctness…
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…
We give a domain-theoretic semantics to a statistical programming language, using the plain old category of dcpos, in contrast to some more sophisticated recent proposals. Remarkably, our monad of minimal valuations is commutative, which…
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…
Domain theory has been developed as a mathematical theory of computation and to give a denotational semantics to programming languages. It helps us to fix the meaning of language concepts, to understand how programs behave and to reason…
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…
Two groups of naturally arising questions in the mathematical theory of domains for denotational semantics are addressed. Domains are equipped with Scott topology and represent data types. Scott continuous functions represent computable…
We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map…
We develop a domain-theoretic framework for imprecise probability reasoning and inference on general topological spaces with a countably based continuous lattice of open sets. We address two distinct forms of uncertainty: partial or…
We investigate partial functions and computability theory from within a constructive, univalent type theory. The focus is on placing computability into a larger mathematical context, rather than on a complete development of computability…
Domain theory is `a mathematical theory that serves as a foundation for the semantics of programming languages'. Domains form the basis of a theory of partial information, which extends the familiar notion of partial function to encompass a…
Recently, J. D. Lawson encouraged the domain theory community to consider the scientific program of developing domain theory in the wider context of $T_0$ spaces instead of restricting to posets. In this paper, we respond to this calling…
We introduce a continuous domain for function spaces over topological spaces which are not core-compact. Notable examples of such topological spaces include the real line with the upper limit topology, which is used in solution of initial…
Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the…
Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened "homotopy type theory". In this…
Domain decomposition methods (DDMs) provide a unifying framework for the scalable numerical solution of partial differential equations. Originating from Schwarz's alternating method, they have evolved into a rich family of algorithms that…