Andrej
Bauer
University of
Ljubljana, Slovenia
How
to Connect the Theory and Practice of Computable Mathematics
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
Friday, April 6, 2007
3:30 p.m.
Wean
Hall 8220
Principles
of Programming Seminars