Category Archives: Publications

Research publications by Andrej Bauer

Realizability as the Connection between Computable and Constructive Mathematics

Abstract:
These are lecture notes for a tutorial seminar which I gave at a satellite seminar of Computability and Complexity in Analysis 2005 in Kyoto. The main message of the notes is that computable mathematics is the realizability interpretation of constructive mathematics. The presentation is targeted at an audience which is familiar with computable mathematics but less so with constructive mathematics, category theory or realizability theory.

Note: I have revised the original version from August 23, 2005 and corrected the horrible error at the beginning of Section 2. I would appreciate reports on other mistakes that you find in these notes.

Download (version of October 16, 2005): c2c.pdf, c2c.ps.gz

The Dedekind Reals in Abstract Stone Duality

With Paul Taylor.

Abstract: Abstract Stone Duality (ASD) is an approach to topology that provides an abstract and conceptually satisfying account of topological spaces. The calculus of ASD reveals the computational content of various topological notions and suggests how to compute with them. The distinguishing feature of ASD is a direct axiomatisation in terms of spaces and maps, which does not rely on an underlying set-theoretic or topos-theoretic foundation.

This paper makes the first step in real analysis within ASD, namely the construction of the real line using two-sided Dedekind cuts. Compactness and overtness of the closed interval are proved, and the arithmetic operations are defined. The ASD calculus gives programs for computing the arithmetic operations and the quantifiers that express compactness and overtness.

As the paper aims to be a self-contained introduction to ASD for those interested in constructive and computable topology and analysis, it includes a rapid survey of the ASD calculus. The foundational background to the calculus was covered in detail in earlier work.

Further topics in real analysis within ASD, such as the Intermediate Value Theorem, are presented in a separate paper by Paul Taylor which builds on this one.

To be presented at Computability and Complexity in Analysis 2005, Kyoto, Japan.

Download: an up-to-date version from Paul Taylor’s Abstract Stone Duality page.

Blog as a repository for research papers

I have created a blog category in which I will stick all my research papers. The idea is to allow people to comment on the papers and have an opportunity for discussion. There are some obvious advantages to this, such as: bug reports, opinions, references to related and relevant topics, a paper and a discussion about it are found in the same place, etc. Right now I do not see any obvious drawbacks, so I hope it will turn out to be a good idea.

First Steps in Synthetic Computability Theory (MFPS XXI)

Abstract: Computability theory, which investigates computable functions and computable sets, lies at the foundation of computer science. Its classical presentations usually involve a fair amount of Gödel encodings which sometime obscure ingenious arguments. Consequently, there have been a number of presentations of computability theory that aimed to present the subject in an abstract and conceptually pleasing way. We build on two such approaches, Hyland’s effective topos and Richman’s formulation in Bishop-style constructive mathematics, and develop basic computability theory, starting from a few simple axioms. Because we want a theory that resembles ordinary mathematics as much as possible, we never speak of Turing machines and Gödel encodings, but rather use familiar concepts from set theory and topology.

Presented at: Mathematical Foundations of Programming Semantics XXI, Birmingham, 2004 (invited talk).

Download paper: synthetic.pdf, synthetic.ps.gz

Download slides: synthetic-slides.pdf