Below are brief summaries of some of my papers, the most recent first, with links into a more complete bibliography with abstracts, citation details and preprint/postprint versions.
(a second paper with Ming Ng and derived from his thesis) "A point-free look at Ostrowski's Theorem and absolute values" applies the geometric techniques of point-free analysis to a fundamental result in algebraic number theory. This is related to Theorem XII.5.1 in the Mines-Richman-Ruitenburg book on Constructive Algebra, but the point-free stress on topology takes it in new directions.
"The Fundamental Theorem of Calculus point-free, with applications to exponentials and logarithms" develops point-free real analysis by showing how to differentiate some maps.
"Generalized point-free spaces, pointwise" explains how to work with toposes by reference to their points, with a dependent type theory of spaces.
(with Ming Ng and derived from his thesis) "Point-free construction of real exponentiation" does just that; logarithms too. It exemplifies the geometric approach to point-free real analysis.
(with Sina Hazratpour) "Fibrations of AU-contexts beget fibrations of toposes" provides new and simpler methods for proving that geometric morphisms are (op-)fibrations.
"Arithmetic universes and classifying toposes" describes how "arithmetic" theories give rise to geometric theories and classifying toposes in a way that allows for variation of the base topos used.
"Arithmetic universes and classifying toposes" describes how "arithmetic" theories give rise to geometric theories and classifying toposes in a way that allows for variation of the base topos used.
"Sketches for arithmetic universes" sets out a formal categorical account of how geometric theories and their classifing toposes might, in enough cases to be useful, be replaced by a finitary logic and arithmetic universes. This programme was originally proposed in "Topical categories of domains".
"The localic compact interval is an Escardó-Simpson interval object" proves a certain universal property for the localic interval.
(with Christopher Townsend) "A coherent account of geometricity" gives a purely categorical description of the notion of geometric construction on bundles.
(with Bertfried Fauser) "Geometric constructions preserve fibrations" gives a geometricity criterion for bundle constructions to preserve fibrations and opfibrations (in the 2-categorical sense).
(with Francesco Ciraulo) "Positivity relations on a locale" explains the binary positivity relations of Sambin's Basic Picture in more purely localic terms, with reference to algebras for the lower powerlocale.
"Domain theory in topical form" describes how "Topical categories of domains" developed out of Abramsky's "Domain theory in logical form".
(with Bas Spitters and Sander Wolters) "Gelfand spectra in Grothendieck toposes using geometric mathematics" uses geometric mathematics to calculate some locales associated with spectral bundles in topos approaches to quantum physics.
"The Born rule as structure of spectral bundles", an extended abstract, outlines how topos approaches to quantum foundations may be understood in terms of a base space of contexts and a bundle where the fibre over a context is its spectrum. The machinery of point-free spaces and geometricty is exploited.
"A monad of valuation locales" develops the mathematics of integration, including Riesz and Fubini theorems, in a localic setting using valuations instead of measures.
"Continuity and geometric logic" gives a broad survey of geometric logic and its unique selling points.
(with Yde Venema and Jacob Vosmaer) "Generalized powerlocales via relation lifting" defines a generalization of the Vietoris powerlocale. For the Vietoris powerlocale itself, the paper gives a new presentation in terms of "nabla", and also proves constructive results regarding compactness.
(with Milly Maietti) "An induction principle for consequence in arithmetic universes" explores some issues, in particular the lack of cartesian closedness, if one uses arithmetic universes instead of Grothendieck toposes to classify (suitable) geometric theories.
(with Achim Jung and Drew Moshier) "Presenting dcpos and dcpo algebras" describes the presentations of dcpo algebras by generators and relations.
"Issues of logic, algebra and topology in ontology" uses geometric logic as a case study for how a logic might be affected by the ontological commitment one is prepared to make.
"Fuzzy sets and geometric logic" describes how geometric logic can provide a conceptual simplification of Hoehle's sheaf approach to fuzzy sets. You can also download slides of my Linz talk on this topic.
"Cosheaves and connectedness in formal topology" gives a predicative introduction to some topos ideas in Bunge and Funk's book "Singular Coverings of Toposes".
"A localic theory of lower and upper integrals" is just what it says.
"The connected Vietoris powerlocale" describes a powerlocale construction whose points are connected, and uses it to give a choice-free constructive account of the Intermediate Value Theorem and Rolle's Theorem.
"Locales and toposes as spaces" is a first step towards a constructive version of "Topology via Logic". It explains how theories in geometric logic can be viewed as topological spaces (for the propositional fragment) or generalized topological spaces (toposes) for the full predicate logic.
(with Erik Palmgren) "Partial Horn logic and cartesian categories" gives a simple presentation of cartesian theories using a logic in which function symbols may be partial. It leads to an easy proof of the free model theorem, and a simple construction of classifying categories.
"Sublocales in formal topology" shows how various results about sublocales in topos-valid locale theory transfer to predicative formal topology.
"Some constructive roads to Tychonoff" uses Tychonoff's theorem as a case study for approaches to topology in constructive mathematics. The final version is published in this book.
(with Gillian Hill) "A language for configuring multi-level specifications" develops "Presheaves as configured specifications" to cope with specifications in which components of systems may themselves be configured systems.
"Localic completion of generalized metric spaces I" shows how generalized metric spaces may be completed to give locales. "Generalized" means esentially that only the zero self-distance and the triangle inequality are expected. "Localic completion of generalized metric spaces II: Powerlocales" investigates their powerlocales, gives a simple description of them as "generalized metric powerspaces", and describes some applications.
"Entailment systems for stably locally compact locales" describes a way of presenting stably locally compact locales using a kind of non-reflexive sequent calculus. It is similar to the Multilingual Sequent Calculus of Jung, Kegelmann and Moshier, but without the explicit presence of conjunction and disjunction in the sequents.
(with Christopher Townsend) "A universal characterization of the double powerlocale" shows that the double powerlocale PP(X) can be considered a double exponential $^($^X) even when X is not locally compact (so $X doesn't exist). It does this using the Yoneda embedding of the category of locales.
"Compactness in locales and in formal topology" describes a general criterion for compactness of a formal topology (with preordered base) and proves it in both topos-valid mathematics and predicative mathematics.
"The double powerlocale and exponentiation: a case study in geometric logic" examines the "double powerlocale", the composite of the upper and lower powerlocales, and relates it to exponentiation. It uses geometric reasoning (stable under pullback along geometric morphisms) to make locales appear like spaces.
(with Pedro Resende) "Localic sup-lattices and tropological systems" resets the quantale methods in a constructive localic framework.
(with Gillian Hill) "Presheaves as Configured Specifications" outlines a specification language for describing how components are put together with sharing. It uses presheaves to give a mathematical treatment that is both simple and specificationally natural.
"Strongly Algebraic = SFP (Topically)" develops the work of "Topical Categories of Domains" to cover the equivalence between two of Plotkin's characterizations of SFP domains. It also serves as an introduction to how presheaf toposes are interpreted as generalized spaces.
"Localic Completion of Quasimetric Spaces" presents a localic account of completion of quasimetric spaces, using Lawvere's approach by enriched categories.
"Topical Categories of Domains" sets domain theory, and in particular Abramsky's account in "Domain Theory in Logical Form", in a framework of geometric logic. Ordinary categories of domains are replaced by "topical" categories, internal in the category of toposes and geometric morphisms: the classes of objects and morphisms are replaced by toposes classifying them.
"Topology via Constructive Logic" presents the idea that constructive mathematics has practical usefulness in studying topology.
"Constructive points of powerlocales" gives a constructively sound account of the points of the lower, upper and Vietoris powerlocales, and shows how in certain cases a powerlocale of D is homeomorphic to $^D.
"Toposes pour les vraiment nuls" is a further introduction to Grothendieck's idea of toposes as generalized topological spaces, using geometric logic to hide topology.
"Toposes pour les nuls" is a brief introduction to Grothendieck's idea of toposes as generalized topological spaces, written from a topological viewpoint.
"Locales are not pointless" presents some preliminary results for reasoning about arbitrary locales through their points, with particular applications to powerlocales.
(With Mark Dawson) "Towards a GeoZ toolkit" discusses how a mathematical toolkit for GeoZ must differ from that for Z, and illustrates the use of schema entailment in presenting it.
"Geometric logic as a specification language" is a short introduction to GeoZ, a Z-like specification language based on geometric logic. Includes a description of "schema entailment" and its use as a definitional mechanism.
"Geometric Logic in Computer Science" is an introduction to geometric logic, paying particular attention to the deep mathematical properties that make it differ from other logics.
(With Samson Abramsky) "Quantales, Observational Logic and Process Semantics" studies quantales (complete lattices equipped with monoid structure, the binary operation distributing over all joins) with applications to process semantics.
"Information Systems for Continuous Posets" defines an "infosys" as an idempotent relation, and shows how they may be used to present continuous dcpos. Includes a proof that the Vietoris powerlocale of a continuous dcpo is again a continuous dcpo.
"Geometric Theories and Databases" describes a topos-theoretic construction of categorical powerdomains (bagtoposes) with tentative application to database theory.
(With Peter Johnstone) "Preframe Presentations Present" investigates preframes (directed complete posets with finite meets that distribute over the directed joins) with applications to locale theory, including an easy proof of the localic Tychonoff theorem.