Category Archives: Talks

Material related to my talks, mostly slides.

Metric Spaces in Synthetic Topology

With Davorin Lešnik.

Abstract: We investigate the relationship between constructive theory of metric spaces and synthetic topology. Connections between these are established by requiring a relationship to exist between the intrinsic and the metric topology of a space. We propose a non-classical axiom which has several desirable consequences, e.g., that all maps between separable metric spaces are continuous in the sense of metrics, and that, up to topological equivalence, a set can be equipped with at most one metric which makes it complete and separable.

Presented at: 3rd Workshop on Formal Topology

Download slides: 3wft.pdf

Implementing real numbers with RZ

With Iztok Kavkler.

Abstract: RZ is a tool which translates axiomatizations of mathematical structures to program specifications using the realizability interpretation of logic. This helps programmers correctly implement data structures for computable mathematics. RZ does not prescribe a particular method of implementation, but allows programmers to write efficient code by hand, or to extract trusted code from formal proofs, if they so desire. We used this methodology to axiomatize real numbers and implemented the specification computed by RZ. The axiomatization is the standard domain-theoretic construction of reals as the maximal elements of the interval domain, while the implementation closely follows current state-of-the-art implementations of exact real arithmetic. Our results shows not only that the theory and practice of computable mathematics can coexist, but also that they work together harmoniously.

Presented at Computability and Complexity in Analysis 2007.

Download paper: rzreals.pdf

Download slides: cca2007-slides.pdf

RZ: a tool for bringing constructive and computable mathematics closer to programming practice

With Chris Stone.

Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

Presented at Computablity in Europe 2007.

Download paper:

Download slides: cie2007-slides.pdf

Download source code from RZ web page.

Continuity Begets Continuity (Frauenwörth slides)

With Alex Simpson.

Abstract: We present a constructive meta-theorem about sequential continuity which allows us to conclude from a constructive proof of existence of a function between complete metric spaces satisfying a given system of (functional) equations that there also exists a sequentially continuous function satisfying the system.

Presented at: Trends in Constructive mathematics, Frauenwörth am Chimsee, Germany, June 2006.

Download slides: continuity_begets_continuity_bavaria_slides.pdf