These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now.
Abstract: Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions [...]
Two versions of this talk were given at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008.
Joint work with Paul Taylor.
Abstract: Cauchy’s construction of reals as sequences of rational approximations is the theoretical basis for a number of implementations of exact real numbers, while Dedekind’s construction of reals as cuts has [...]
With Iztok Kavkler.
Abstract: The interval domain was proposed by Dana Scott as a domain-theoretic model for real numbers. It is a successful theoretical idea which also inspired a number of computational models for real numbers. However, current state-of-the-art implementations of real numbers, e.g., Mueller’s iRRAM and Lambov’s RealLib, do not seem to be based on [...]
A tutorial presented at the Mathematical Foundations of Programming Semantics XXIII Tutorial Day.
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 [...]
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 [...]
With Chris Stone.
Abstract:
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. [...]
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, [...]
With Chris Stone.
Presented at: Reliable Implementation of Real Number Algorithms: Theory and Practice, Dagstuhl Seminar 06021.
Abstract: see “Specifications via Realizability (CLASE)”.
Talk notes: rz-dagstuhl.pdf (handwritten notes of the talk with examples of how RZ works)
At the EST training workshop in Fischbachau, Germany, I gave two lectures on syntehtic computability theory. This version of the talk contains material on recursive analysis which is not found in the MFPS XXI version of a similar talk.
Abstract:
Computability theory, which investigates computable functions and computable sets, lies at the foundation of logic and computer [...]