With Davorin Lešnik.
Abstract: We investigate the relationship between the synthetic approach to topology, in which every set is equipped with an intrinsic topology, and constructive theory of metric spaces. We relate the synthetic notion of compactness of Cantor space to Brouwer’s Fan Principle. We show that the intrinsic and metric topologies of complete separable metric spaces coincide if they do so for Baire space. In Russian Constructivism the match between synthetic and metric topology breaks down, as even a very simple complete totally bounded space fails to be compact, and its topology is strictly finer than the metric topology. In contrast, in Brouwer’s intuitionism synthetic and metric notions of topology and compactness agree.
Download paper: csms_in_synthtop.pdf
Abstract: In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt theorem and Tarskiâ€™s fixed-point theorem for chain-complete lattices do not have constructive (topos-valid) proofs.
Published in: Theoretical Computer Science Volume 430, 27 April 2012, Pages 43–50. Mathematical Foundations of Programming Semantics (MFPS XXV)
With Iztok Kavkler.
Abstract: We formulate a predicative, constructive theory of continuous domains whose realizability interpretation gives a practical implementation of continuous Ï‰-chain complete posets and continuous maps between them. We apply the theory to implementation of the interval domain and exact real numbers.
With Iztok Kavkler.
Abstract: RZ is a tool which translates axiomatizations of mathematical structures to program speciï¬cations 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 speciï¬cation 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
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 slides: cie2007-slides.pdf
Download source code from RZ web page.