Steve Vickers: Bibliography

Steven Vickers: Bibliography

This is a complete list of my academic papers, with abstracts and dowloadable preprint versions where available.

Elsewhere, you can also find -

Note on .ps papers

Some of the older .ps papers (PreFrPrePre, GeoTh+DBs, Infosys and QuProc) have been prepared from original Microsoft Word documents. They will differ from the published versions, certainly in format and perhaps also in details of content. Also, some of those .ps files have not been tested on a printer, so please report any problems with them by emailing me (s.j.vickers) at

Contents (most recent first)


"Arithmetic universes and classifying toposes"


Draft version Jan 2017: pdf.
Archived at arXiv:1701.04611

Structures in Vickers's category $\mathfrak{Con}$, of certain sketches for arithmetic universes (AUs, i.e. list arithmetic pretoposes), are shown to give rise to base-free results of elementary toposes (with nno), geometric theories and classifying toposes.
Categories of models (strict or non-strict) of contexts $\mathbb{T}$ in AUs are acted on strictly on the left by non-strict AU-functors and strictly on the right by context maps, and the actions combine in a strict action of a Gray tensor product.
Given a context extension $\mathbb{T}_0 \subset \mathbb{T}_1$, for any model $M$ of $\mathbb{T}_0$ in an elementary topos $\mathcal{S}$ with nno there is a geometric theory $\mathbb{T}_1/M$ of $\mathbb{T}_1$-models restricting to $M$, and it has a classifying topos $\mathcal{S}[\mathbb{T}_1/M]$. This construction is ``geometric'' in the sense that for any geometric morphism $f\colon \mathcal{S}' \to \mathcal{S}$, the classifier $\mathcal{S}'[\mathbb{T}_1/f^\ast M]$ is got by pseudopullback of $\mathcal{S}[\mathbb{T}_1/M]$ along $f$.
This is treated in a fibrational way by considering a 2-category $\mathfrak{GTop}$ of Grothendieck toposes (bounded geometric morphisms) fibred (as bicategory) over a 2-category $\mathfrak{Top}_{\cong}$ of elementary toposes with nno, geometric morphisms, and natural isomorphisms. The notion of classifying topos as representing object for a split fibration is then fibred over variable base using fibrations ``locally representable'' over a second fibration.

Maths Subject Classification 18B25; 18D05 18D30 18C30 03G30
Keywords: geometric theory, 2-fibration, sketch, Gray tensor

"Sketches for arithmetic universes"

Submitted for publication.

Draft version August 2016: pdf.
Archived at arXiv:1608.01559.

A theory of sketches for arithmetic universes (AUs) is developed.
A restricted notion of sketch, called here context, is defined with the property that every non-strict model is uniquely isomorphic to a strict model. This allows us to reconcile the syntactic, dealt with strictly using universal algebra, with the semantic, in which non-strict models must be considered.
For any context $\mathbb{T}$, a concrete construction is given of the AU $\mathbf{AU}\langle\mathbb{T}\rangle$ freely generated by it.
A 2-category $\mathfrak{Con}$ of contexts is defined, with a full and faithful 2-functor to the 2-category of AUs and strict AU-functors, given by $\mathbb{T} \mapsto \mathbf{AU}\langle\mathbb{T}\rangle$. It has finite pie limits, and also all pullbacks of a certain class of "extension" maps. Every object, morphism or 2-cell of $\mathfrak{Con}$ is a finite structure.
Maths Subject Classification 18C30; 03G30

See also the OASIS talk.

"The localic compact interval is an Escardó-Simpson interval object"


Preprint version June 2015: pdf.

The locale corresponding to the real interval $[-1,1]$ is an interval object, in the sense of Escard\'{o} and Simpson, in the category of locales. The map $c\colon 2^\omega \to [-1,1]$, mapping a stream $s$ of signs $\pm 1$ to $\Sigma_{i=1}^\infty s_i 2^{-i}$, is a proper localic surjection; it is also expressed as a coequalizer.

"A coherent account of geometricity"

(Steven Vickers and Christopher Townsend)


Preprint version April 2014: pdf.

A "bundle endofunctor preserving proneness" for a cartesian category $\mathcal{C}$ is an endofunctor $\mathfrak{T}_\bullet$ of the arrow category $\mathcal{C}^{\downarrow}$, the identity on codomains, that preserves the property of morphisms of being pullback squares. Such a $\mathfrak{T}_\bullet$ is "slicewise strong", restricting to a strong endofunctor $\mathfrak{T}_\bullet$ on every slice $\mathcal{C}/B$, and with that structure preserved by pullback between slices.
In the other direction, a strong endofunctor $T$ on $\mathcal{C}$ extends to a bundle endofunctor $T_\bullet$ on $\mathcal{C}$, which preserves proneness if $T$ preserves coreflexive equalizers.
If a bundle endofunctor $\mathfrak{T}_\bullet$ preserving proneness also preserves coreflexive equalizers, then it is naturally isomorphic to the $T_\bullet$ arising from $T = \mathfrak{T}_1$.
Combining these, bundle endofunctors for $\mathcal{C}$ preserving proneness and coreflexive equalizers are equivalent to strong endofunctors on $\mathcal{C}$ preserving coreflexive equalizers; this latter structure is inherited by all slices and preserved by pullback between them.
The results extend to situations where $\mathfrak{T}_\bullet$ and $T$ are monads.
We propose that the structure of bundle endofunctor preserving proneness is a satisfactory categorical abstraction of the notion of geometric construction when $\mathcal{C}$ is the category $\mathbf{Loc}$ of locales. The powerlocales give rise to bundle monads on $\mathbf{Loc}$ preserving proneness and coreflexive equalizers; likewise for the covariant powerobject monad on any topos.

"Geometric constructions preserve fibrations"

(Bertfried Fauser and Steven Vickers)


Archived at arXiv:1411.2457.

Let $\mathcal{C}$ be a representable 2-category, and $\mathfrak{T}_\bullet$ a 2-endofunctor of the arrow 2-category $\mathcal{C}^\downarrow$ such that (i) $\mathsf{cod} \mathfrak{T}_\bullet = \mathsf{cod} \colon \mathcal{C}^\downarrow \rightarrow \mathcal{C}$ and (ii) $\mathfrak{T}_\bullet$ preserves proneness (cartesianness) of morphisms in $\mathcal{C}^\downarrow$. Then $\mathfrak{T}_\bullet$ preserves fibrations and opfibrations in $\mathcal{C}$. The proof takes Street's characterization of (e.g.) opfibrations as pseudoalgebras for 2-monads $\mathfrak{L}_B$ on slice categories $\mathcal{C}/B$ and develops it by defining a 2-monad $\mathfrak{L}_\bullet$ on $\mathcal{C}^\downarrow$ that takes change of base into account, and uses known results on the lifting of 2-functors to pseudoalgebras.

"Positivity relations on a locale"

(Francesco Ciraulo and Steven Vickers)

Annals of Pure and Applied Logic 167 (2016), pp. 806-819
(special issue for articles on the topics of the 4th Workshop on Formal Topology (4WFTop), Ljubljana 2012)
Published on-line 20-Apr-2016

ISSN 0168-0072,

Final submitted version January 2015: pdf.

This paper analyses the notion of a positivity relation of Formal Topology from the point of view of the theory of Locales. It is shown that a positivity relation on a locale corresponds to a suitable class of points of its lower powerlocale. In particular, closed subtopologies associated to the positivity relation correspond to overt (that is, with open domain) weakly closed sublocales. Finally, some connection is revealed between positivity relations and localic suplattices (these are algebras for the powerlocale monad).

"Domain theory in topical form"

In Coecke, Ong, Panangaden (ed.) "Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky"
Springer LNCS 7860 (2013), pages 348--349

ISSN 0302-9743, ISBN 978-3-642-38163-8,

Preprint version: pdf.

Describes how "Topical categories of domains" developed out of Abramsky's "Domain theory in logical form".

"Gelfand spectra in Grothendieck toposes using geometric mathematics"

(Bas Spitters, Steven Vickers and Sander Wolters)

In Proceedings of the 9th International Workshop on Quantum Physics and Logic (QPL 2012), Brussels 2012 (ed. Duncan, Panangaden).
Electronic Proceedings in Theoretical Computer Science 158 (2014), pp. 77 - 107.
ISSN 2075-2180, doi:10.4204/EPTCS.158.7

Preprint version: pdf, or arXiv 1310.0705.

In the topos approach to quantum theory by Heunen, Landsman and Spitters, one associates to any unital C*-algebra A, a topos T(A) of sheaves on a locale and a commutative C*-algebra A within that topos. The Gelfand spectrum of A is a locale Σ in this topos, which is equivalent to a bundle over the base locale. We further develop this external presentation of the locale Σ, by noting that the construction of the Gelfand spectrum in a general topos can be described using geometric logic. As a consequence, the spectrum, seen as a bundle, is computed fibrewise.
As a by-product of the geometricity of Gelfand spectra, we find an explicit external description of the spectrum whenever the topos is a functor category. As an intermediate result we show that locally perfect maps compose, so that the externalization of a locally compact locale in a topos of sheaves over a locally compact locale is locally compact, too.

"The Born rule as structure of spectral bundles"

(Extended abstract)
(Bertfried Fauser, Guillaume Raynaud and Steven Vickers)

In Proceedings of the 8th International Workshop on Quantum Physics and Logic (QPL 2011), Nijmegen 2011 (ed. Jacobs, Selinger, Spitters).
Electronic Proceedings in Theoretical Computer Science 95 (2012), pp. 81 - 90.
ISSN 2075-2180, doi:10.4204/EPTCS.95.8

Preprint version: pdf

Topos approaches to quantum foundations are described in a unified way by means of spectral bundles, where the base space is a space of contexts and each fibre is its spectrum. Differences in variance are due to the the bundle being a fibration or opfibration. Relative to this structure, the probabilistic predictions of the Born rule in finite dimensional settings are then described as a section of a bundle of valuations. The construction uses in an essential way the geometric nature of the valuation locale monad.

"A monad of valuation locales"

Preprint version: pdf

If X is a locale then its valuation locale has for its points the valuations on X. This construction is the functor part of a strong monad on the category of locales, a localic analogue of the Giry monad. It is commutative, i.e. product valuations exist and a Fubini Theorem holds. An analogue of the Riesz Representation theorem holds. Concrete representations are given for the tensor product of lattices and for the modular monoid. The work conforms with the constructive constraints of geometric logic.

"Continuity and geometric logic"

Journal of Applied Logic 12 (1) (2014), pages 14-27

ISSN: 1570-8683; doi: 10.1016/j.jal.2013.07.004.

Preprint version: pdf
Reports my Bordeaux talk "Aspects of geometric logic".

This paper is largely a review of known results about various aspects of geometric logic. Following Grothendieck's view of toposes as generalized spaces, one can take geometric morphisms as generalized continuous maps. The constructivist constraints of geometric logic guarantee the continuity of maps constructed, and can do so from two different points of view: for maps as point transformers and maps as bundles.

"Generalized powerlocales via relation lifting"

(Yde Venema, Steven Vickers and Jacob Vosmaer)

Mathematical Structures in Computer Science 23 (1) (2013), pages 142-199.

ISSN: 0960-1295; doi: 10.1017/S0960129512000229.

Preprint version: pdf

This paper introduces an endofunctor VT on the category of frames, parametrized by an endofunctor T on the category Set that satisfies certain constraints. This generalizes Johnstone's construction of the Vietoris powerlocale, in the sense that his construction is obtained by taking for T the finite covariant power set funtor. Our construction of the T-powerlocale VT L out of a frame L is based on ideas from coalgebraic logic and makes explicit the connection between the Vietoris construction and Moss's coalgebraic cover modality.

We show how to extend certain natural transformations between set functors to natural transformations between T-powerlocale functors. Finally, we prove that the operation VT preserves some properties of frames, such as regularity, zero-dimensionality, and the combination of zerodimensionality and compactness.

"An induction principle for consequence in arithmetic universes"

(Maria Emilia Maietti and Steven Vickers)

Journal of Pure and Applied Algebra 216 (8-9) (2012), pages 2049-2067.

ISSN: 0022-4049; doi: 10.1016/j.jpaa.2012.02.040.

Preprint version: pdf
Presentations: Amsterdam and Genova.

Suppose in an arithmetic unverse we have two predicates φ and ψ for natural numbers, satisfying a base case φ(0)→ψ(0) and an induction step that, for generic n, the hypothesis φ(n)→ ψ(n) allows one to deduce φ(n+1)→ ψ(n+1). Then it is already true in that arithmetic universe that (∀ n)(φ(n)→ ψ(n)). This is substantially harder than in a topos, where cartesian closedness allows one to form an exponential φ(n)→ ψ(n).

The principle is applied to the question of locatedness of Dedekind sections.

The development analyses in some detail a notion of "subspace" of an arithmetic universe, including open or closed subspaces and a boolean algebra generated by them. There is a lattice of subspaces generated by the opens and the closeds, and it is isomorphic to the free Boolean algebra over the distributive lattice of subobjects of 1 in the arithmetic universe.

"Presenting dcpos and dcpo algebras"

(Achim Jung, M. Andrew Moshier and Steven Vickers)

In Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV) (ed. Bauer, Mislove), Electronic Notes in Theoretical Computer Science 218 (2008), pp. 209 - 229.
ISSN 1571-0661; doi:10.1016/j.entcs.2008.10.013

Preprint version: pdf

Dcpos can be presented by a preorder of generators and inequational relations expressed as covers. Algebraic operations on the generators (possibly with their results being ideals of generators) can be extended to the dcpo presented, provided the covers are "stable" for the operations. The resulting dcpo algebra has a natural universal characterization and satisfies all the inequational laws satisfied by the generating algebra.

Applications include known "coverage theorems" from locale theory.

"Issues of logic, algebra and topology in ontology"

Chapter 22 in "Theory and Applications of Ontology: Computer Applications" (ed. Poli, Healy, Kameas), vol. 2 of "Theory and Applications of Ontology", Springer, 2010.
ISBN 978-90-481-8846-8
Copyright Springer.

Preprint version: pdf

When one uses a particular logical formalism, one makes an ontological commitment to being able to interpret the symbols involved. We discuss this in a case study of geometric logic, being aided by a presentation of the logic as a sequent calculus. We also discuss the connections of geometric logic with topology and algebra.

"Fuzzy sets and geometric logic"

Fuzzy Sets and Systems 161 (2010), pp. 1175 - 1204.
ISSN 0165-0114; doi: 10.1016/j.fss.2009.06.013.

Preprint version: pdf

Hoehle has identified fuzzy sets, valued in a frame (complete Heyting algebra) Ω, with certain sheaves over Ω: the subsheaves of constant sheaves More general sheaves can be got as quotients of the fuzzy sets. His principal approach to sheaves over Ω, and topos-theoretic constructions on them, is via complete Ω-valued sets.

In this paper we show how the geometric fragment of those constructions can be described in a natural "stalkwise" manner, provided one works also with incomplete Ω-valued sets.

Our exposition examines in detail the interactions between different technical expressions of the notion of sheaf, and highlights a conceptual view of sheaf as "continuous set-valued map".

You can also view my slides for the invited talk I gave on this topic at the 29th Linz Seminar on Fuzzy Set Theory, February 2008.

"Cosheaves and connectedness in formal topology"

Annals of Pure and Applied Logic 163 (2012), pp. 157-174.
ISSN 0168-0072; doi:10.1016/j.apal.2011.06.024

Preprint version: pdf

The localic definitions of cosheaves, connectedness and local connectedness are transferred from impredicative topos theory to predicative formal topology. A formal topology is locally connected (has base of connected opens) iff it has a cosheaf π0 together with certain additional structure and properties that constrain π0 to be the connected components cosheaf. In the inductively generated case, complete spreads (in the sense of Bunge and Funk) corresponding to cosheaves are defined as formal topologies. Maps between the complete spreads are equivalent to homomorphisms between the cosheaves. A cosheaf is the connected components cosheaf for a locally connected formal topology iff its complete spread is a homeomorphism, and in this case it is a terminal cosheaf.

A new, geometric proof is given of the topos-theoretic result that a cosheaf is a connected components cosheaf iff it is a "strongly terminal" point of the symmetric topos, in the sense that it is terminal amongst all the generalized points of the symmetric topos. It is conjectured that a study of sites as "formal toposes" would allow such geometric proofs to be incorporated into predicative mathematics.

Key words: Formal topology, predicative, locally connected, cosheaf, symmetric topos, complete spread
2008 MSC: Primary 03F60; Secondary 54D05, 54B20, 18F10

"A localic theory of lower and upper integrals"

Mathematical Logic Quarterly 54 (1) (2008), pp. 109 - 123.
ISSN 0942-5616 (print), 1521-3870 (online); doi:10.1002/malq.200710028

Preprint version: pdf

An account of lower and upper integration is given. It is constructive in the sense of geometric logic. If the integrand takes its values in the non-negative lower reals, then its lower integral with respect to a valuation is a lower real. If the integrand takes its values in the non-negative upper reals, then its upper integral with respect to a covaluation and with domain of integration bounded by a compact subspace is an upper real. Spaces of valuations and of covaluations are defined.

Riemann and Choquet integrals can be calculated in terms of these lower and upper integrals.

"The connected Vietoris powerlocale"

Topology and its Applications 156 (2009), pp. 1886-1910.
ISSN: 0166-8641; doi:10.1016/j.topol.2009.03.043

Preprint version: pdf

The Vietoris powerlocale VX is a point-free analogue of the Vietoris hyperspace. In this paper we introduce and study a sublocale VcX whose points are those points of VX that (considered as sublocales of X) satisfy a constructively strong connectedness property. VcX is a strong monad on the category of locales. The strength gives rise to a product map
x: VcX x VcY -> Vc(X x Y),
showing that the product of two of these connected sublocales is again connected. If X is locally connected then VcX is overt. In the case where X is the localic completion of a generalized metric space Y, the points of VcX are characterized as certain Cauchy filters of formal balls for the finite power set FY with respect to a Vietoris metric.

The results are applied to the particular case of the point-free real line, giving a choice-free constructive version of the Intermediate Value Theorem and Rolle's Theorem.

The work is constructive in the sense of topos-validity with natural numbers object. Its geometric aspects (preserved under inverse image functors) are stressed, and exploited to give a pointwise development of the point-free locale theory. The connected Vietoris powerlocale itself is a geometric construction.

"Locales and toposes as spaces"

Chapter 8 in "Handbook of Spatial Logics" (ed. Aiello, Pratt-Hartman, van Bentham), Springer, 2007, pp. 429-496.
ISBN 978-1-4020-5586-7
Copyright Springer Science + Business Media B.V.

Preprint version: pdf

This chapter was written as an introduction for logicians to the spatial content of geometric logic.

It first outlines the established ideas of Lindenbaum algebras of logical theories, and how they combine with Stone duality (between Boolean algebras and Stone topological spaces) to give a correspondence between theories in classical propositional logic and Stone spaces. This enables one to treat logical theories as topological spaces.

The aim of the chapter is to show how the same insights can be applied to geometric logic, whose connectives mirror the axioms of topology, even though its incompleteness means there is no exact Stone duality.

An important part of this is the role of constructive reasoning. This is paradoxical, since without classical principles (such as choice) it becomes even harder to find the models needed to show completeness. However, constructive reasoning can be applied to models in non-classical mathematics, and in particular the internal mathematics of sheaves. This has the effect of allowing access to a sufficiency of models.

The chapter also describes how the same principles apply to theories in predicate geometric logic. However, the spaces are now generalized in Grothendieck's sense as toposes. The chapter describes how the categorical technicalities of topos theory (e.g. in Mac Lane and Moerdijk) connects to the spatial intuitions.

"Partial Horn logic and cartesian categories"

(Erik Palmgren and Steven Vickers)

Annals of Pure and Applied Logic 145 (3) (2007), pp. 314 - 353.
ISSN: 0168-0072; doi:10.1016/j.apal.2006.10.001

Preprint version: pdf

A logic is developed in which function symbols are allowed to represent partial functions. It has the usual rules of logic (in the form of a sequent calculus) except that the substitution rule has to be modified. It is developed here in its minimal form, with equality and conjunction, as "partial Horn logic".

Various kinds of logical theory are equivalent:

  • partial Horn theories
  • "quasi-equational" theories, partial Horn theories without predicate symbols
  • cartesian theories
  • essentially algebraic theories

The logic is sound and complete with respect to models in $\mathbf{Set}$, and sound with respect to models in any cartesian (finite limit) category.

The simplicity of the quasi-equational form allows an easy predicative constructive proof of the free partial model theorem for cartesian theories: that if a theory morphism is given from one cartesian theory to another, then the forgetful (reduct) functor from one model category to the other has a left adjoint.

Various examples of quasi-equational theory are studied, including those of cartesian categories and of other classes of categories. For each quasi-equational theory $\mathbb{T}$ another, $\mathrm{Cart}\varpi\mathbb{T}$, is constructed, whose models are cartesian categories equipped with models of $\mathbb{T}$. Its initial model, the "classifying category" for $\mathbb{T}$, has properties similar to those of the syntactic category, but more precise with respect to strict cartesian functors.

MSC: Primary 18C10. Secondary 03C05, 03G30, 08A55, 08B05, 08B20, 18C05.

Keywords: Cartesian theory, essentially algebraic, free algebra, classifying category, syntactic category, partial algebra.

"Sublocales in formal topology"

Journal of Symbolic Logic 72 (2) (2007) 463-482
ISSN: 0022-4812; doi:10.2178/jsl/1185803619

Preprint version: pdf

The paper studies how the localic notion of sublocale transfers to formal topology. For any formal topology (not necessarily with positivity predicate) we define a sublocale to be a cover relation that includes that of the formal topology. The family of sublocales has set-indexed joins. For each set of base elements there are corresponding open and closed sublocales, boolean complements of each other. They generate a boolean algebra amongst the sublocales. In the case of an inductively generated formal topology, the collection of inductively generated sublocales has coframe structure.

Overt sublocales and weakly closed sublocales are described, and related via a new notion of "rest closed" sublocale to the binary positivity predicate. Overt, weakly closed sublocales of an inductively generated formal topology are in bijection with "lower powerpoints", arising from the impredicative theory of the lower powerlocale.

Compact sublocales and fitted sublocales are described. Compact fitted sublocales of an inductively generated formal topology are in bijection with "upper powerpoints", arising from the impredicative theory of the upper powerlocale.

"Some constructive roads to Tychonoff"

In: Laura Crosilla and Peter Schuster (eds.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, pp. 223 - 238. Oxford Logic Guides 48, Oxford University Press (2005).
ISBN: 0-19-856651-4. Click here for more details.

Preprint version: pdf

The Tychonoff Theorem is discussed with respect to point-free topology, from the point of view of both topos-valid and predicative mathematics.

A new proof is given of the infinitary Tychonoff Theorem using predicative, choice-free methods for possibly undecidable index set. It yields a complete description of the finite basic covers of the product.

"A language for configuring multi-level specifications"

(Gillian Hill and Steven Vickers)

Final journal version appeared as:

Theoretical Computer Science 351 (2006) 146 - 166
ISSN: 0304-3975; doi:10.1016/j.tcs.2005.09.065

The preprint version is closer to the original conference version, in:

Rattray, C., Maharaj, S. and Shankland, C. (eds) Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland, pp. 196-210. Springer Lecture Notes in Computer Science 3116 (2004).
ISBN 3-540-22381-9

Preprint version: ps

This paper shows how systems can be built from their component parts with specified sharing. Its principle contribution is a modular language for configuring systems. A configuration is a description in the new language of how a system is constructed hierarchically from specifications of its component parts. Category theory has been used to represent the composition of specifications that share a component part by constructing colimits of diagrams. We reformulated this application of category theory to view both configured specifications and their diagrams as algebraic presentations of presheaves. The framework of presheaves leads naturally to a configuration lanaguage that expresses structuring from instances of specifications, and also incorporates a new notion of instance reduction from a particular configuration . The language now expresses the hierarchical structuring of multi-level configured specifications. The syntax is simple because it is independent of any specification language; structuring a diagram to represent a configuration is simple because there is no need to calculate a colimit; and combining specifications is simple because structuring is by configuration morphisms with no need to flatten either specifications or their diagrams to calculate colimits.

"Localic completion of generalized metric spaces II: Powerlocales"

(Steven Vickers)

Journal of Logic and Analysis 1(11) (2009) pp. 1-48.
ISSN: 1759-9008; doi:10.4115/jla.2009.1.11

Preprint version: pdf

(This paper is a greatly revised version of part of "Localic completion of quasimetric spaces".)

The work investigates the powerlocales (lower, upper, Vietoris) of localic completions of generalized metric spaces. The main result is that all three are localic completions of generalized metric powerspaces, on the Kuratowski finite powerset. This is a constructive, localic version of spatial results of Bonsangue et al. and of Edalat and Heckmann.

As applications, a localic completion is always open, and is compact iff its generalized metric space is totally bounded.

The representation is used to discuss closed intervals of the reals, with the localic Heine-Borel Theorem as a consequence.

The work is constructive in the topos-valid sense.

Keywords: locale, constructive, topos, metric, hyperspace, powerlocale.
AMS Subject Code Classifications: Primary -- 54B20. Secondary -- 06D22, 03G30, 54E50, 03F60.

"Localic completion of generalized metric spaces I"

(Steven Vickers)

Theory and Applications of Categories 14 (2005), pp. 328-356.
ISSN: 1201-561X.

Free on-line at TAC: pdf

(This paper is a greatly revised version of part of "Localic completion of quasimetric spaces".)

We give a constructive localic account of the completion of generalized metric spaces (gms's) in a sense derived from that of Lawvere: a set X equipped with a metric map from X2 to the interval of upper reals (approximated from above but not from below) from 0 to infinity inclusive, and satisfying the zero self-distance law and the triangle inequality. The completion is then a locale whose points can be viewed either as Cauchy filters of formal balls or (following Lawvere's approach using enriched categories) as flat left modules.

Non-expansive functions between the gms's lift to continuous maps between the completions.

Various examples and constructions are given, including finite products.

The points of this completion are classically equivalent to those of the "Yoneda completion" of Bonsangue et al., modified to use Cauchy nets instead of sequences.

The exposition is constructive in the topos-valid sense and exploits the use of geometric reasoning to approach locales and toposes as "topology-free spaces".

"Entailment systems for stably locally compact locales"

(S.J. Vickers)

Theoretical Computer Science 316 (2004) (special issue on Domain Theory) pp. 259-296.
ISSN: 0304-3975; doi:10.1016/j.tcs.2004.01.033

Preprint version: pdf, ps

The category $\mathbf{SCFr}_U$ of stably continuous frames and preframe homomorphisms (preserving finite meets and directed joins) is dual to the Karoubi envelope of a category $\mathbf{Ent}$ whose objects are sets and whose morphisms $X \rightarrow Y$ are upper closed relations between the finite powersets $\mathcal{F}X$ and $\mathcal{F}Y$. Composition of these morphisms is the "cut composition" of Jung et al. that interfaces disjunction in the codomains with conjunctions in the domains, and thereby relates to their multi-lingual sequent calculus. Thus stably locally compact locales are represented by "entailment systems" $(X,\vdash)$ in which $\vdash$, a generalization of entailment relations, is idempotent for cut composition.

Some constructions on stably locally compact locales are represented in terms of entailment systems: products, duality and powerlocales.

Relational converse provides $\mathbf{Ent}$ with an involution, and this gives a simple treatment of the duality of stably locally compact locales. If $A$ and $ B$ are stably continuous frames, then the internal preframe hom $A \pitchfork B$ is isomorphic to $\hat{A} \otimes B$ where $\hat{A}$ is the Hofmann-Lawson dual.

For a stably locally compact locale $X$, the lower powerlocale of $X$ is shown to be the dual of the upper powerlocale of the dual of $X$.

"A universal characterization of the double powerlocale"

(S.J. Vickers + C.F. Townsend)

Theoretical Computer Science 316 (2004) (special issue on Domain Theory) pp. 297-321.
ISSN: 0304-3975; doi:10.1016/j.tcs.2004.01.034

Preprint version: pdf

The double powerlocale $\mathbb{P}(X)$ (found by composing, in either order, the upper and lower powerlocale constructions $P_U$ and $P_L$) is shown to be isomorphic in $[\mathbf{Loc}^{op}, \mathbf{Set}]$ to the double exponential $\mathbb{S}^{\mathbb{S}^X}$ where $\mathbb{S}$ is the Sierpinski locale. Further, $P_U(X)$ and $P_L(X)$ are shown to be the subobjects of $\mathbb{P}(X)$ comprising, respectively, the meet semilattice and join semilattice homomorphisms. A key lemma shows that, for any locales $X$ and $Y$, natural transformations from $\mathbb{S}^X$ (the presheaf $\mathbf{Loc}(- \times X, \mathbb{S})$) to $\mathbb{S}^Y$ (i.e. $\mathbf{Loc}(- \times Y, \mathbb{S})$) are equivalent to dcpo morphisms from the frame $\Omega(X)$ of $X$ to that of $Y$. It is also shown that $\mathbb{S}^X$ has a localic reflection in $[\mathbf{Loc}^{op}, \mathbf{Set}]$ whose frame is $\mathbf{dcpo}(\Omega(X), \Omega(Y))$.

The reasoning is constructive in the sense of topos validity.

"Compactness in locales and in formal topology"

(S.J. Vickers)

Annals of Pure and Applied Logic 137 (2006), pp. 413-438. (Special issue for the Proceedings of the 2nd Workshop on Formal Topology, Venice 2002.)
ISSN: 0168-0072; doi:10.1016/j.apal.2005.05.028

Preprint version: pdf

If a locale is presented by a "flat site", it is shown how its frame can be presented by generators and relations as a dcpo. A necessary and sufficient condition is derived for compactness of the locale (and also for its openness). Although its derivation uses impredicative constructions, it is also shown predicatively using the inductive generation of formal topologies.

A predicative proof of the binary Tychonoff theorem is given, including a characterization of the finite covers of the product by basic opens. The discussion is then related to the double powerlocale.

"The double powerlocale and exponentiation: a case study in geometric logic"

(S.J. Vickers)

Theory and Applications of Categories 12 (2004) pp. 372-422

Free on-line at TAC: pdf

If $X$ is a locale, then its double powerlocale $\mathbb{P}(X)$ is defined to be $P_U(P_L(X))$ where $P_U$ and $P_L$ are the upper and lower powerlocale constructions. We prove various results relating it to exponentiation of locales, including the following. First, if $X$ is a locale for which the exponential $\mathbb{S}^X$ exists (where $\mathbb{S}$ is the Sierpinski locale), then $\mathbb{P}(X)$ is an exponential $\mathbb{S}^{\mathbb{S}^X}$. Second, if in addition $W$ is a locale for which $\mathbb{P}(W)$ is homeomorphic to $\mathbb{S}^X$, then $X$ is an exponential $\mathbb{S}^W$.

The work uses geometric reasoning, i.e. reasoning stable under pullback along geometric morphisms, and this enables the locales to be discussed using their points as though they were spaces. It relies on a number of geometricity results including those for locale presentations and for powerlocales.

"Localic sup-lattices and tropological systems"

(P. Resende + S.J. Vickers)

Theoretical Computer Science 305 (2003) (special issue on Topology in Computer Science) pp. 311-346.
ISSN: 0304-3975; doi:10.1016/S0304-3975(02)00702-8

Preprint version: ps, pdf

The approach to process semantics using quantales and modules is topologized by considering tropological systems whose sets of states are replaced by locales and which satisfy a suitable stability axiom. A corresponding notion of localic sup-lattice (algebra for the lower powerlocale monad) is described, and it is shown that there are contravariant functors from sup-lattices to localic sup-latices and, for each quantale Q, from left Q-modules to localic right Q-modules. A proof technique for third completeness due to Abramsky and Vickers is reset constructively, and an example of application to failures semantics is given.

"Presheaves as Configured Specifications"

(S.J.Vickers + G.A.Hill)

Formal Aspects of Computing 13 (2001) pp. 32-49.
ISSN: 0934-5043 (printed), 1433-299X (electronic); doi:10.1007/PL00003938

Preprint version: ps

The paper addresses a notion of configuring systems, constructing them from specified component parts with specified sharing. This notion is independent of any underlying specification language and has been abstractly identified with the taking of colimits in category theory. Mathematically it is known that these can be expressed by presheaves and the present paper applies this idea to configuration.

We interpret the category theory informally as follows. Suppose C is a category whose objects are interpreted as specifications, and for which each morphism u: X -> Y is interpreted as contravariant "instance reduction", reducing instances of specification Y to instances of X. Then a presheaf P over C represents a collection of instances that is closed under reduction. We develop an algebraic account of presheaves in which we present configurations by generators (for components) and relations (for shared reducts), and we outline a proposed configuration language based on the techniques. Oriat uses diagrams to express colimits of specifications, and we show that Oriat's category Diag(C) of finite diagrams is equivalent to the category of finitely presented presheaves over C.

"Strongly Algebraic = SFP (Topically)"

Mathematical Structures in Computer Science 11 (2001) pp. 717-742.

ISSN 0960-1295; doi:10.1017/S0960129501003437

Preprint version: ps, pdf

Certain "Finite Structure Conditions" on a geometric theory are shown to be sufficient for its classifying topos to be a presheaf topos. The conditions assert that every homomorphism from a finite structure of the theory to a model factors via a finite model, and they hold in cases where the finitely presentable models are all finite.

The conditions are shown to hold for the theory of strongly algebraic (or SFP) information systems and some variants, as well as for some other theories already known to be classified by presheaf toposes.

The work adheres to geometric constructivism throughout and in consequence provides "topical" categories of domains (internal in the category of toposes and geometric morphisms) with an analogue of Plotkin's double characterization of strongly algebraic domains, by sets of minimal upper bounds and by sequences of finite posets.

"Localic Completion of Quasimetric Spaces"

Research Report DoC 97/2, Department of Computing, Imperial College (1998).
(This has now been superseded by "Localic completion of generalized metric spaces I" and "Localic completion of generalized metric spaces II: Powerlocales".)

Preprint version: pdf

We give a constructive localic account of the completion of quasimetric spaces. In the context of Lawvere's approach, using enriched categories, the points of the completion are flat left modules over the quasimetric space. The completion is a triquotient surjective image of a space of Cauchy sequences and can also be embedded in a continuous dcpo, the "ball domain". Various examples and constructions are given, including the upper, lower and Vietoris powerlocales, which are completions of finite powerspaces. The exposition uses the language of locales as "topology-free spaces".

"Topical Categories of Domains"

Mathematical Structures in Computer Science 9 (1999) pp.569-616.
ISSN 0960-1295; doi:10.1017/S0960129599002741

Preprint version: ps, pdf

It is shown how many techniques of categorical domain theory can be expressed in the general context of topical categories (where "topical" means internal in the category Top of Grothendieck toposes with geometric morphisms). The underlying topos machinery is hidden by using a geometric form of constructive mathematics, which enables toposes as "generalized topological spaces" to be treated in a transparently spatial way, and also shows the constructivity of the arguments. The theory of strongly algebraic (SFP) domains is given as a case study in which the topical category is Cartesian closed.

Properties of local toposes and of lifting of toposes (sconing) are summarized, and it is shown that the category of toposes has a fixpoint object in the sense of Crole and Pitts. This is used to show that for a local topos, all endomaps have initial algebras, and this provides a general context in which to describe fixpoint constructions including the solution of domain equations involving constructors of mixed variance. Covariance with respect to embedding-projection pairs or adjunctions arises in a natural way.

The paper also provides a summary of constructive results concerning Kuratowski finite sets, including a novel strong induction principle; and shows that the topical categories of sets, finite sets and decidable sets are not Cartesian closed (unlike the cases of finite decidable sets and strongly algebraic domains).

"Topology via Constructive Logic"

Moss, Ginzburg and de Rijke (eds) "Logic, Language and Computation Vol II" (Proceedings of conference on Information-Theoretic Approaches to Logic, Language, and Computation, 1996). CSLI Publications, Stanford (1999) pp. 336-345.
ISBN 1575861801; 157586181X

Preprint version: ps, pdf

By working constructively in the sense of geometric logic, topology can be hidden. This applies also to toposes as generalized topological spaces.

"Toposes pour les vraiment nuls"

In : Edalat, Jourdan and McCusker (eds) "Theory and Formal Methods 1996", Third Imperial College Department of Computing Workshop on Theory and Formal Methods, April 1996, pp. 1-12. Imperial College Press, London, 1996.
ISBN 1-86094-031-5

Postprint version: ps, pdf

Restriction to geometric logic can enable one to define topological structures and continuous maps without explicit reference to topologies. This idea is illustrated with some examples and used to explain toposes as generalized topological spaces.

"Constructive points of powerlocales"

Mathematical Proceedings of the Cambridge Philosophical Society 122 (1997), 207-222.
ISSN 0305-0041; doi:10.1017/S0305004196001636

Preprint version: ps, pdf

Results of Bunge and Funk and of Johnstone, providing constructively sound descriptions of the global points of the lower and upper powerlocales, are extended here to describe the generalized points and proved in a way that displays in a symmetric fashion two complementary treatments of frames: as suplattices and as preframes. We then also describe the points of the Vietoris powerlocale.

In each of two special cases, an exponential $^D ($ being the Sierpinski locale) is shown to be homeomorphic to a powerlocale: to the lower powerlocale when D is discrete, and to the upper powerlocale when D is compact regular.

"Toposes pour les nuls"

In: "Semantics Society Newsletter, Issue 4", 1995.Also available as Research Report DoC 96/4, Department of Computing, Imperial College (1996).

Preprint version: ps, pdf

An introduction to Grothendieck's idea of toposes as generalized topological spaces.

Sheaves are described as continuous set-valued functions, geometric morphisms are described as continuous maps, and continuity itself is explained as "genericity + geometricity".

"Reasoned Programming"

(K. Broda + S. Eisenbach + H. Khoshnevisan + S. Vickers)

Prentice Hall International Series in Computer Science (1994).

ISBN 0-13-098831-6

Downloadable version: pdf

Aimed at first or second year undergraduate students, Reasoned Programming shows how to apply mathematical reasoning to the development of the computer programs that users need, using logical specifications to express these and then writing program code to achieve the objectives set out in the specifications.

The book starts with functional programming (including tutorial material written for Miranda) for its simplicity, but also shows how it can be used as a reasoning tool for imperative programming.

"Locales are not pointless"

In: Hankin, Mackie and Nagarajan (eds) "Theory and Formal Methods of Computing 1994", 199-216, Imperial College Press.
ISBN 1-86094-003-X

Preprint version: ps, ps.gz, pdf

The Kripke-Joyal semantics is used to interpret the fragment of intuitionistic logic containing conjunction, implication, equality and universal quantification in the category of locales. An axiomatic theory is developed that can be interpreted soundly in two ways, using either lower or upper powerlocales, so that pairs of separate results can be proved as single formal theorems.

Openness and properness of maps between locales are characterized by descriptions using the logic, and it is proved that a locale is open iff its lower powerlocale has a greatest point. The entire account is constructive and holds for locales over any topos.

"Geometric logic as a specification language"

In: Hankin, Mackie and Nagarajan (eds) "Theory and Formal Methods of Computing 1994", 321-340, Imperial College Press.
ISBN 1-86094-003-X

Preprint version: ps.gz, pdf

The "observational content" of geometric logic is discussed and it is proposed that geometric logic is an appropriate basis for a Z-like specification language in which schemas are used as geometric theory presentations.

A descriptional mechanism of "schema entailment", generalizing type constructions and logical entailment, is defined and investigated in some examples, and is also used in defining schema morphisms which are discussed briefly in connection with schema connectives, and with specifying and implementing operations.

"Towards a GeoZ toolkit"

(M. Dawson + S.J. Vickers)

In: Hankin, Mackie and Nagarajan (eds) "Theory and Formal Methods of Computing 1994", Imperial College Press.
ISBN 1-86094-003-X

Preprint version: ps.gz, pdf

The use of Geometric Logic as the foundation of a specification language called GeoZ is proposed elsewhere. In this note we explore GeoZ from the perspective of practitioners, already familiar with the existing Z notation, by explaining the issues that arise and the role of schema entailment in the GeoZ reformulation of Z's mathematical toolkit.

"Geometric Logic in Computer Science"

pp. 37-54 in G.L. Burn, S.J. Gay and M.D. Ryan (eds) "Theory and Formal Methods 1993", Proceedings of the first Imperial College Department of Computing workshop on Theory and Formal Methods, Springer Workshops in Computer Science, 1993.
ISBN 3-540-19842-3; 0-387-19842-3

Preprint version: ps.gz, ps, pdf

We present an introduction to geometric logic and the mathematical structures associated with it, such as categorical logic and toposes. We also describe some of its applications in computer science including its potential as a logic for specification languages.

"Quantales, Observational Logic and Process Semantics"

(S. Abramsky + S.J. Vickers)

pp.161-227 in Mathematical Structures in Computer Science vol. 3 (1993).

Preprint version: ps.gz, pdf

Various notions of observing and testing processes are placed in a uniform algebraic framework in which observations are taken as constituting a quantale. General completeness criteria are stated, and proved in our applications.

NB - An earlier version of this paper was issued as a Departmental Report. The new version is substantially revised in its discussion and its mathematical techniques, though the overall approach is unchanged.

"Information Systems for Continuous Posets"

pp. 201-229 in "Theoretical Computer Science B" vol. 114, (1993)
ISSN 0304-3975; doi:10.1016/0304-3975(93)90072-2

Preprint version: ps.gz, pdf

NB - This paper was previously entitled "Continuous Information Systems". It has been renamed to avoid confusion with Raymond Hoofman's paper.

The method of information systems is extended from algebraic posets to continuous posets by taking a set of tokens with an ordering that is transitive and interpolative but not necessarily reflexive. This develops results of Raney on completely distributive lattices and of Hoofman on continuous Scott domains, and also generalizes Smyth's "R-structures". Various constructions on continuous posets have neat descriptions in terms of these continuous information systems; here we describe Hoffmann-Lawson duality (which could not be done easily with R-structures) and Vietoris power locales. We also use the method to give a partial answer to a question of Johnstone's: in the context of continuous posets, Vietoris algebras are the same as localic semilattices.

"Geometric Theories and Databases"

pp. 288-314 in M.P. Fourman, P.T. Johnstone and A.M. Pitts (eds) "Applications of Categories in Computer Science" (Proceedings of the LMS Symposium, Durham 1991), London Mathematical Society Lecture Note Series 177, Cambridge University Press, 1992.
ISBN 0-521-42726-6

Preprint version: pdf

Domain theoretic understanding of databases as elements of powerdomains is modified to allow multisets of records instead of sets. This is related to geometric theories and classifying toposes, and it is shown that algebraic base domains lead to algebraic categories of models in two cases analogous to the lower (Hoare) powerdomain and Gunter's mixed powerdomain.

"Preframe Presentations Present"

(P. Johnstone + S.J. Vickers)

pp. 193-212 in A. Carboni, M.C. Pedicchio and G. Rosolini (eds.) Category Theory - Proceedings, Como 1990 (Springer Lecture Notes in Mathematics 1488,1991).
ISBN 3-540-54706-1; 0-387-54706-1; doi:10.1007/BFb0084221

Preprint version: pdf

Preframes (directed complete posets with finite meets that distribute over the directed joins) are the algebras for an infinitary essentially algebraic theory, and can be presented by generators and relations. This result is combined with a general argument concerning categories of commutative monoids to give a very short proof of the localic Tychonoff Theorem. It is also shown how frames can be presented as preframes, a result analogous to Johnstone's construction of frames from sites, and an application is given.

"Formal Implementation"

Chapter = 25 in J.A. McDermid (ed.) The Software Engineer's Reference Book, (Butterworth Scientific, London, 1991).
ISBN 0-750-61040-9

An account of the formal logic of pre- and post-conditions.

"Topology via Logic"

Cambridge Tracts in Theoretical Computer Science 5 (Cambridge University Press 1988).
ISBN 0-521-36062-5; 0-521-57651-2

An advanced textbook on topology for computer scientists with three unusual features. First, the introduction is from a localic viewpoint, motivated by the logic of finite observations: this provides a more direct approach than the traditional one based on abstracting properties of open sets in the real line. Second, the methods of locale theory are freely exploited. Third, there is a substantial discussion of some computer science applications. Although books on topology aimed at mathematics exist, not book has been written specifically for computer scientists, and as computer scientists become more aware of the mathematical foundations of their discipline, it is appropriate that such topics are presented in a form of direct relevance and applicability. This book goes some way towards bridging the gap.

"A fixpoint construction of the p-adic domain"

pp. 270-289 in D.H. Pitt, A. Poigne and D.E. Rydeheard, Category Theory and Computer Science (Proceedings of Edinburgh Workshop, 1986) (Springer Lecture Notes in Computer Science 283, 1987).
ISBN 3-540-18508-9; 0-387-18508-9

The Kahn domain on p symbols can be given an arithmetic structure so that its maximal elements are isomorphic to the p-adic integers. This is described as a fixpoint of a functor in a category of sheaves of rings.

"An algorithmic approach to the p-adic integers"

pp. 599-616 in M. Main, A. Melton, M. Mislove and D. Schmidt Mathematical Foundations of Programming Language Semantics (Proceedings of Tulane Workshop, 1987) (Springer Lecture Notes in Computer Science 298, 1988).
ISBN 3-540-19020-1; 0-387-19020-1

The ring of p-adic integers can be embedded as the maximal elements in a Scott domain with algebraic structure. We show how definitions and proofs in the mathematical theory of p-adics can be replaced by algorithms on the partial elements and formal programming methods working on the algorithms. Certain types of argumetns translate naturally into non-deterministic algorithms using the Smyth power domain.

"Theories as Categories"

(M.P. Fourman + S.J. Vickers)

pp. 434-448 in D. Pitt, S. Abramsky, A. Poigné and D. Rydeheard (eds.) Category Theory and Computer Programming (Springer Lecture Notes in Computer Science 240, 1986).
ISBN 3-540-17162-2; 0-387-17162-2

This paper is not, and is not intended to be, original. Its purpose is to present a couple of examples from the folklore of topos theory, the theory of classifying topoi in particular. This theory and its applications spread initially without the benefit of widespread publication. Many ideas were spread among a relatively small group, largely by word of mouth. The result of this is that the literature does not provide an accessible introduction to the subject. Computer scientists studying the logic of computing have recently become interested in this area. They form our intended audience. In the space (and time) available we can only hope to provide a small selection of the many ideas missing from, or buried in, the literature. We attempt to give a perspective of the structure of the subject. Our selection is, of necessity, idiosyncratic, and our treatment brief. We hope that missing technical details may be reconstructed from the literature. This may require some diligence. [Yes, it did - SJV]

To apportion credit for the ideas presented here is difficult so long after the event. Lawvere and Joyal have a special position in htis subject. Their intuitions have shaped it. Many others, who participated in the Peripatetic Seminars in Europe, the New York Topos Theory Seminar (which also wandered) and the Category Theory meetings at Oberwohlfach, contributed also. Their contributions are, in general, better reflected in their published works. Finally, to apportion blame, this paper derives from notes taken by SJV of a talk by MPF. Any misrepresentations are the responsibility of the latter.

Back to top