University of Ljubljana, Slovenia

Abstract:

Usually there is a certain amount of discrepancy, or at least lack of connection, between a theoretical mathematical model and its practical implementation. For example, in the name of efficiency we might implement a structure with a different set of basic operations than those that the theory axiomatizes, or we might calculate with floating point numbers where the theory assumes reals. Once the formal connection between a mathematical model and its implementation is lost, it is not clear how we might verify correctness of implementation, or what that even means.

One way to keep the connection is to use a tool, such as Coq, that extracts trusted code from formal roofs. While this has proved very successful in many respects, it does not allow programmers to freely write the most efficient code, or to easily use programming constructs that do not correspond to proofs under the propositions-as-types interpretation (such as exceptions, parallelism and store).

We developed a tool, called RZ, which allows us to take the middle ground between theory and practice. Using the realizability interpretation, RZ generates specifications (ML signatures with assertions) from axiomatizations of theories written in constructive logic with dependent types, subtypes and quotients, but does not translate proofs to code. Instead, programmers can implement the specifications in any way they see fit.

In this talk I will discuss various issues related to RZ, including suggestions on how to extend the ML module system to allow more flexible handling of theories and specifications. I will also report on our experience with using RZ to implement exact real arithmetic that follows a formal specification based on a domain-theoretic model of reals, and whose efficiency is comparable to that of current state-of-the-art implementations of exact real arithmetic.

Joint
work with:

Chris
Stone

Computer Science Department

Harvey Mudd College

Iztok Kavkler

Faculty of Mathematics & Physics

University of Ljubljana

Computer Science Department

Harvey Mudd College

Iztok Kavkler

Faculty of Mathematics & Physics

University of Ljubljana

Friday, April 6, 2007

3:30 p.m.

Wean Hall 8220

Principles
of Programming Seminars