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

By Andrej Bauer, on January 21st, 2007

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. By [...]

January 21st, 2007 | Category: Publications, RZ, Talks | 3 comments

Continuity Begets Continuity (Frauenwörth slides)

By Andrej Bauer, on August 15th, 2006

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, [...]

August 15th, 2006 | Category: Constructive math, Talks | Leave a comment

Specifications via Realizability (Dagstuhl)

By Andrej Bauer, on January 13th, 2006

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 [...]

January 13th, 2006 | Category: Talks | Leave a comment

First Steps in Synthetic Computability Theory (Fischbachau)

By Andrej Bauer, on September 18th, 2005

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. [...]

September 18th, 2005 | Category: Synthetic computability, Talks | 8 comments

Realizability as the Connection between Computable and Constructive Mathematics

By Andrej Bauer, on August 23rd, 2005

Lecture notes for my tutorial at Computability and Complexity in Analysis 2005, Kyoto. [...]

August 23rd, 2005 | Category: Publications, Talks | 12 comments

First Steps in Synthetic Computability Theory (MFPS XXI)

By Andrej Bauer, on May 8th, 2005

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 [...]

May 8th, 2005 | Category: Publications, Synthetic computability, Talks | One comment

Specifications via Realizability (CLASE 2005)

By Andrej Bauer, on April 9th, 2005

How to build specifications for abstract data types using realizability [...]

April 9th, 2005 | Category: Publications, RZ, Talks | Leave a comment
« Newer Entries