Category Archives: Talks

Material related to my talks, mostly slides.

First Steps in Synthetic Computability Theory (Fischbachau)

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 science. Its classical presentations usually involve a fair amount of Goedel encodings. 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 Goedel encodings, but rather use familiar concepts from set theory and
topology.

Download slides: est.pdf

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

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

Specifications via Realizability (CLASE 2005)

With Chris Stone.

Abstract:
We present a system, called RZ, for automatic generation of program specifications from mathematical theories. We translate mathematical theories to specifications by computing their realizability interpretations in the ML language augmented with assertions (as comments). While the system is best suited for descriptions of those data structures that can be easily described in mathematical language (e.g., finitely presented groups, real arithmetic, graphs, etc.), it also elucidates the relationship between data structures and constructive mathematics.

Presented at:
Constructive Logic for Automated Software Engineering (CLASE), Satellite event of ETAPS 2005, Edinburgh, 9th April 2005

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

Download slides:
rz-slides.pdf