Abstract The results of Section 3.1 of the 2017 paper “Isomorphism Theorems between Models of Mixed Choice” need an additional assumption when $\bullet$ is “ $1$ .” If $\bullet$ is nothing or “ $\leq 1$ ,” no change is needed. Also, the mistake only applies to the angelic cases, namely to the maps $r_{{\mathtt {A}}{\mathtt {P}}}$ and $s^\bullet _{{\mathtt {A}}{\mathtt {P}}}$ ; the demonic cases $r_{{\mathtt {D}}{\mathtt {P}}}$ and $s^\bullet _{{\mathtt {D}}{\mathtt {P}}}$ are unaffected. If $\bullet$ is “ $1$ ,” and in the angelic cases, instead of just assuming that $\mathcal L X$ is locally convex, we need to additionally assume that $X$ is compact, or that $\mathcal L X$ is locally convex-compact, sober, and topological – for example, if $X$ is core-compact – or that $X$ is LCS-complete, namely, a homeomorph of a $G_\delta$ subspace of a locally compact sober space.

We show that every continuous valuation on a locally convex, locally convex-compact, sober topological cone $\mathfrak{C}$ has a barycenter. This barycenter is unique, and the barycenter map $\beta$ is continuous, hence is the structure map of a $\mathbf V_{\mathrm w}$-algebra, i.e., an Eilenberg-Moore algebra of the extended valuation monad on the category of $T_0$ topological spaces; it is, in fact, the unique $\mathbf V_{\mathrm w}$-algebra that induces the cone structure on $\mathfrak{C}$.

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 allows for program transformations that permute the order of independent random draws, as one would expect. A similar property is not known for Jones and Plotkin’s monad of continuous valuations. Instead of working with true real numbers, we work with exact real arithmetic, providing a bridge towards possible implementations (implementations by themselves are not addressed here). Rather remarkably, we show that restricting ourselves to minimal valuations does not restrict us much: All measures on the real line can be modeled by minimal valuations on the domain I ℝ ⊥ of exact real arithmetic. We give three operational semantics for our language, and we show that they are all adequate with respect to the denotational semantics. We also explore quite a few examples to demonstrate that our semantics computes exactly as one would expect and to debunk the myth that a semantics based on continuous maps would not be expressive enough to encode measures with non-compact support using only measures with compact support, or to encode measures via non-continuous density functions, for instance. Our examples also include some useful, non-trivial cases of distributions on higher-order objects.

Abstract We show analogues of the Daniell–Kolmogorov and Prohorov theorems on the existence of projective limits of measures, in the setting of continuous valuations on T0 topological spaces.

Abstract We give two concrete examples of continuous valuations on dcpo’s to separate minimal valuations, point-continuous valuations, and continuous valuations: (1) Let ${\mathcal J}$ be the Johnstone’s non-sober dcpo, and μ be the continuous valuation on ${\mathcal J}$ with μ(U)=1 for nonempty Scott opens U and μ(U)=0 for $U=\emptyset$ . Then, μ is a point-continuous valuation on ${\mathcal J}$ that is not minimal. (2) Lebesgue measure extends to a measure on the Sorgenfrey line $\mathbb{R}_\ell$ . Its restriction to the open subsets of $\mathbb{R}_\ell$ is a continuous valuation λ. Then, its image valuation $\overline\lambda$ through the embedding of $\mathbb{R}_\ell$ into its Smyth powerdomain $\mathcal{Q}\mathbb{R}_\ell$ in the Scott topology is a continuous valuation that is not point-continuous. We believe that our construction $\overline\lambda$ might be useful in giving counterexamples displaying the failure of the general Fubini-type equations on dcpo’s.

Abstract We define representations for downward-closed subsets of a rich family of well-quasi-orders, and more generally for closed subsets of an even richer family of Noetherian topological spaces. This includes the cases of finite words, of multisets, of finite trees, notably. Those representations are given as finite unions of ideals, or more generally of irreducible closed subsets. All the representations we explore are computable, in the sense that we exhibit algorithms that decide inclusion, and compute finite unions and finite intersections. The origin of this work lies in the need for computing finite representations of sets of successors of the downward closure of one state, or more generally of a downward-closed set of states, in a well-structured transition system, and this is where we start: we define adequate notions of completions of well-quasi-orders, and more generally, of Noetherian spaces. For verification purposes, we argue that the required completions must be ideal completions, or more generally sobrifications, that is, spaces of irreducible closed subsets.

There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract-and those two primitives are required for that.

We give a semantics for a classical variant of Dale Miller and Alwen Tiu’s logic FOλ∇. Our semantics validates the rule that nabla x implies exists x, but is otherwise faithful to the authors’ original intentions. The semantics is based on a category of so-called nabla sets, which are simply strictly increasing sequences of non-empty sets. We show that the logic is sound for that semantics. Assuming there is a unique base type ι, we show that it is complete for Henkin structures, incomplete for standard structures in general, but complete for standard structures in the case of Π1 formulae, and that includes all first-order formulae.

Given a poset $P$, the set, $\Gamma(P)$, of all Scott closed sets ordered by inclusion forms a complete lattice. A subcategory $\mathbf{C}$ of $\mathbf{Pos}_d$ (the category of posets and Scott-continuous maps) is said to be $\Gamma$-faithful if for any posets $P$ and $Q$ in $\mathbf{C}$, $\Gamma(P) \cong \Gamma(Q)$ implies $P \cong Q$. It is known that the category of all continuous dcpos and the category of bounded complete dcpos are $\Gamma$-faithful, while $\mathbf{Pos}_d$ is not. Ho & Zhao (2009) asked whether the category $\mathbf{DCPO}$ of dcpos is $\Gamma$-faithful. In this paper, we answer this question in the negative by exhibiting a counterexample. To achieve this, we introduce a new subcategory of dcpos which is $\Gamma$-faithful. This subcategory subsumes all currently known $\Gamma$-faithful subcategories. With this new concept in mind, we construct the desired counterexample which relies heavily on Johnstone's famous dcpo which is not sober in its Scott topology.

Using the notion of formal ball, we present a few new results in the theory of quasi-metric spaces. With no specific order: every continuous Yoneda-complete quasi-metric space is sober and convergence Choquet-complete hence Baire in its $d$-Scott topology; for standard quasi-metric spaces, algebraicity is equivalent to having enough center points; on a standard quasi-metric space, every lower semicontinuous $\bar{\mathbb{R}}_+$-valued function is the supremum of a chain of Lipschitz Yoneda-continuous maps; the continuous Yoneda-complete quasi-metric spaces are exactly the retracts of algebraic Yoneda-complete quasi-metric spaces; every continuous Yoneda-complete quasi-metric space has a so-called quasi-ideal model, generalizing a construction due to K. Martin. The point is that all those results reduce to domain-theoretic constructions on posets of formal balls.

We relate the so-called powercone models of mixed non-deterministic and probabilistic choice proposed by Tix, Keimel, Plotkin, Mislove, Ouaknine, Worrell, Morgan and McIver, to our own models of previsions. Under suitable topological assumptions, we show that they are isomorphic. We rely on Keimel's cone-theoretic variants of the classical Hahn–Banach separation theorems, using functional analytic methods, and on the Schröder–Simpson Theorem.

In this paper, we propose a categorical framework for bisimulations and unfoldings that unifies the classical approach from Joyal and al. via open maps and unfoldings. This is based on a notion of categories accessible with respect to a subcategory of path shapes, i.e., for which one can define a nice notion of trees as glueing of paths. We prove that transitions systems and pre sheaf models are a particular case of our framework. We also prove that in our framework, several characterizations of bisimulation coincide, in particular an "operational one" akin to the standard definition in transition systems. Also, accessibility is preserved by coreflexions. We then design a notion of unfolding, which has good properties in the accessible case: its is a right adjoint and is a universal covering, i.e., initial among the morphisms that have the unique lifting property with respect to path shapes. As an application, we prove that the universal covering of a groupoid, a standard construction in algebraic topology, coincides with an unfolding, when the category of path shapes is well chosen.

The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be "equivalent" to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be "equivalent" to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.

We give a short and elementary proof of the Schröder–Simpson Theorem, which states that the space of all continuous maps from a given space X to the non-negative reals with their Scott topology is the cone-theoretic dual of the probabilistic powerdomain on X .

We introduce the domain of continuous random variables (CRV) over a domain, as an alternative to Jones and Plotkin's probabilistic power domain. While no known Cartesian-closed category is stable under the latter, we show that the so-called thin (uniform) CRVs define a strong monad on the Cartesian-closed category of bc-domains. We also characterize their inequational theory, as (fair-)coin algebras. We apply this to solve a recent problem posed by M. Escardo: testing is semi-decidable for EPCF terms. CRVs arose from the study of the second author's (layered) Hoare indexed valuations, and we also make the connection apparent.

We establish Choquet–Kendall–Matheron theorems on non-Hausdorff topological spaces. This typical result of random set theory is profitably recast in purely topological terms using intuitions and tools from domain theory. We obtain three variants of the theorem, each one characterising distributions, in the form of continuous valuations, over relevant powerdomains of demonic, angelic and erratic non-determinism, respectively.

Is there any cartesian-closed category of continuous domains that would be closed under Jones and Plotkin's probabilistic powerdomain construction? This is a major open problem in the area of denotational semantics of probabilistic higher-order languages. We relax the question, and look for quasi-continuous dcpos instead. These retain many nice properties from continuous dcpos. We introduce a natural class of such quasi-continuous dcpos, the omega-QRB-domains. We show that they form a category omega-QRB with pleasing properties: omega-QRB is closed under the probabilistic powerdomain functor, has all finite products, all bilimits, and is stable under retracts, and even under so-called quasi-retracts. But... omega-QRB is not cartesian closed.

First-order logic models of security for cryptographic protocols, based on variants of the Dolev–Yao model, are now well-established tools. Given that we have checked a given security protocol π using a given first-order prover, how hard is it to extract a formally checkable proof of it, as require d in, e.g., common criteria at the highest evaluation level (EAL7)? We demonstrate that this is surprisingly hard in the general case: the problem is non-recursive. Nonetheless, we show that we can instead extract finite models M from a set S of clauses representing π, automatically, and give two ways of doing so. We then define a model-checker testing M⊧S, and show how we can instrument it to output a formally checkable proof, e.g., in Coq. Experience on a number of protocols shows that this is practical, and that even complex (secure) protocols modulo equational theories have small finite models, making our approach suitable.

We introduce convex–concave duality for various models of non-deterministic choice, probabilistic choice and the two of them combined. This complements the well-known duality of stably compact spaces in a pleasing way: convex–concave duality swaps angelic and demonic choice, and leaves probabilistic choice invariant.

First-order logic models of security for cryptographic protocols, based on variants of the Dolev-Yao model, are now well-established tools. Given that we have checked a given security protocol pi using a given first-order prover, how hard is it to extract a formally checkable proof of it, as required in, e.g., common criteria at evaluation level 7? We demonstrate that this is surprisingly hard: the problem is non-recursive in general. On the practical side, we show how we can extract finite models M from a set S of clauses representing pi, automatically, in two ways. We then define a model-checker testing M |= S, and show how we can instrument it to output a formally checkable proof, e.g., in Coq. This was implemented in the h1 tool suite. Experience on a number of protocols shows that this is practical.

Logical relations and their generalisations are a fundamental tool in proving properties of lambda calculi, for example, for yielding sound principles for observational equivalence. We propose a natural notion of logical relations that is able to deal with the monadic types of Moggi's computational lambda calculus. The treatment is categorical, and is based on notions of subsconing, mono factorisation systems and monad morphisms. Our approach has a number of interesting applications, including cases for lambda calculi with non-determinism (where being in a logical relation means being bisimilar), dynamic name creation and probabilistic systems.

A topological space is Noetherian iff every open is compact. Our starting point is that this notion generalizes that of well-quasi order, in the sense that an Alexandroff-discrete space is Noetherian iff its specialization quasi-ordering is well. For more general spaces, this opens the way to verifying infinite transition systems based on non-well quasi ordered sets, but where the preimage operator satisfies an additional continuity assumption. The technical development rests heavily on techniques arising from topology and domain theory, including sobriety and the de Groot dual of a stably compact space. We show that the category Nthr of Noetherian spaces is finitely complete and finitely cocomplete. Finally, we note that if X is a Noetherian space, then the set of all (even infinite) subsets of X is again Noetherian, a result that fails for well-quasi orders.

Continuous valuations have been proposed by several authors as a way of modelling probabilistic non-determinism in programming language semantics. Let is algebraic, where every continuous valuation is the sup of a directed family of simple valuations based on finite elements. We exhibit another class of spaces in which every continuous valuation is quasi-simple, the so-called finitarily coherent spaces – in this case there is a largest extension to the Alexandroff topology. In general, the extension to the Alexandroff topology is not unique, unless, for example, the original valuation is bicontinuous. We also show that other natural spaces of valuations, namely those of discrete valuations and point-continuous valuations, can be characterised by similar extension theorems.

International audience

While unification in the simple theory of types (a.k.a. higher-order logic) is undecidable. we show that unification in the pure ramified theory of types with integer levels is decidable. Since pure ramified type theory is not very expressive, we examine the impure case, which has an undecidable unification problem already at order 2. In impure ramified higher-order logics, expressive predicative second-order subsystems of arithmetic or of inductive theories have concise axiomatisations; because of this and our decidability result for the pure case, we argue that ramified systems are expressive higher-order frameworks in which automated proof search should be practical.

Proves that rigid E/spl I.oarr/-unifiability, a decision problem invented by Gallier et al. (1987) to extend first-order tableaux-like proof procedures to first-order logic with equality, is DEXPTIME-complete; and that, when restricted to monadic terms, it is PSPACE-complete.>