The workshop will be held at the campus of the Radboud
University Nijmegen (formerly known as University of Nijmegen or
Catholic University of Nijmegen).
This workshop is part of the TYPES project. We have received financial support both from this project and from NWO.
Topics include, but are not limited to:
There will also be a friendly competition for investigating the state of the art in the various implementations of exact real arithmetic.
The workshop will be free of charge.
The lunches (October 3 and 4) and the dinner (on October 3 and 4) have to be paid by the participants themselves. They will be organised by the organisation committee.
The costs for each participant is:
The workshop will be held at 3th and 4th of October.
|09:30-10:30||Norbert Müller(invited speaker)||Concepts for implementing exact real arithmetic|
|11:00-11:30||Branimir Lambov||RealLib: an Efficient Implementation of Exact Real Arithmetic|
|11:30-12:00||Yann Kieffer||Introducing the COMP project|
|14:00-15:00||Erik Palmgren||Constructive problems in elementary homotopy theory|
|15:30-16:00||Freek Wiedijk||Putting the MathXpert architecture on top of the HOL framework|
|16:00-16:30||Bas Spitters||Almost periodic functions, constructively|
|16:30-17:00||Yves Bertot||Coinductive implementation of Linear Fractional Transformations|
|09:30-10:30||Martín Escardó (invited speaker)||Semantics of programming languages with built-in
abstract data types for exact real numbers
|11:00-11:30||Roland Zumkeller||Verification of inequalities over real numbers|
|11:30-12:00||Russell O'Connor||An Approach to Fast Real Arithmetic in Coq|
|14:00-14:30||Paul Zimmerman||MPFR: recent and future developments|
|Yann Kieffer||First test-drive of COMP|
|A.A.Kahnban||Solving differential equations with imprecise input|
|17:00-17:30||Presentation of the competition||common room|
The program of the workshop is still not finalized, and the second day might end later than in the current table.
University of Birmingham
I'll review some results and open questions on operational
and denotational semantics of programming languages with
abstract data types for real-numbers, by myself and others,
where real numbers are taken in the sense of recursion
theory or of constructive mathematics.
Positive results include computational adequacy (good match of the operational and denotational semantics), an invariance result for the notion of computability at higher types, and a universality result for a family of languages (all computable function(al)s of all orders are programmable).
Partial results include the coincidence of the ‘abstract' or extensional approach with the intensional approach up to order two (where e.g. integration functionals live). The coincidence from order three onwards is open, but there are interesting results in this direction, which reduce the problem to a purely topological question.
A negative result on ‘sequential' computation in the presence of data abstraction has bad consequences regarding efficient implementation of such languages.
Thus, a major open problem is how to reconcile data abstraction with efficiency, so that such languages can be used in practice. It has been shown that the negative effect can be overcome to some extent by the introduction of a certain form of non-determinism, but much work remains to be done in this area. Several questions and problems in this direction will be formulated in the talk.
FB IV - Abteilung Informatik - Universitaet Trier
An implementation of exact arithmetic on the real numbers has to fulfill many (antithetic) demands: On the one hand, its use must be as easy as possible, handling of exact reals should be similar to ordinary floating point numbers. The implementation has to be very efficient, close to the speed of the hardware. Imperative programming languages are still state of the art for numerical purposes. On the other hand, computability on real numbers deals with infinite objects and infinite computations. Multi-valued functions are needed to relax continuity constraints, also lazy evaluation can be advantageous. Limits of sequences are the basis for calculus and numerical analysis, which must be reflected in an implementation. In this talk, we will explain how the iRRAM package for exact real arithmetic tries to match many of these points: For simple applications, it is almost as fast as interval packages based on double precision floating points numbers, but smoothly extends to cases where fixed precision is not enough and exact reals simplify programming.
TU Darmstadt, FB Mathematik
We will explain the theoretical background to the RealLib library for exact real number arithmetic and some of the practical problems that have arised during the development of the library along with the solutions we have used.
COMP stands for ‘Collection Of Mathematical Programs'. But the COMP project aims further than just providing software: its main goal is to give creedence to the motto that ‘Constructive Mathematics equal Computable Mathematics'.
The first subgoal is to show that abstraction can be profitably reconciled with usability. For COMP, it means that using a pure functional language (Haskell) doesn't hurt too much the timings, while allowing further progress: more conceptual algorithms, code more easily proven, support for more abstract objects and computing.
As of now, only real numbers and basic operations on them are implemented. In this talk, I will try to show what the original approach of COMP means both conceptually and in practice, as compared to other efforts towards exact real numbers.
Department of Mathematics, Uppsala University
We consider the problem of constructivising elementary homotopy theory, and how it may be resolved using fo rmal topology.
Radboud University Nijmegen
A implementation of constructive real numbers already exists for Coq from the C-Corn project; however, this implementation is not optimized for speed. My project is to implement a reasonably fast constructive real number library, a nd prove the functions are equivalent to the C-Corn functions.
I will discuss the approach I intend to take, and examine a Haskell prototype. Comments and criticisms will be welcome.
Radboud University Nijmegen
The sum of two periodic functions need not be periodic. Consider for example the sum of the functions sin(x) and sin(sqrt(2)x). Fortunately, such a sum is almost periodic and much of the (Fourier) theory of periodic functions carries over. Unfortunately, constructively matters are complicated by the fact that the almost periodic functions form an inseparable normed space. As such, it has been a challenge for constructive mathematicians to find a natural treatment of them. In this talk we will present a simple constructive proof of Bohr's fundamental theorem for almost periodic functions which we then generalise to almost periodic functions on general topological groups.
Ecole Polytechnique, Paris
The proof of the Kepler conjecture given by Thomas C. Hales in 1998 makes intensive use of computer calculations. In particular, it relies on the correctness of many inequalities over real numbers. For this purpose a formalization of interval arithmetic with some refinements, such as branch-and-bound and monotonicity checks, is presented. The ultimate goal of this work is to develop a reflectional Coq tactic for real inequalities and its correctness proof.
Radboud University Nijmegen
The MathXpert computer algebra system is one of the few computer algebra systems that tries to be logically sound. It implements basic algebra and analysis on the high school level, and for educational purposes is as faithful to high school textbooks as possible.
MathXpert gives its users 1702 ‘operations' that can be applied to expressions inside the system. We will show that it is easy to mimic the MathXpert architecture inside the HOL Light proof assistant, so that one gets MathXpert-style ‘operations' available there as well, but with the advantage that they also generate proofs, so that the correctness of the algebraic manipulations will be guaranteed by the proof assistant.
INRIA Sophia Antipolis
The aim of this talk is to study how Haskell programs manipulating exact representations of real numbers can be encoded in the Coq system in a way that ensures both that the code can be extracted and that its correctness properties can be proved. The main inspirations come from the work of Edalat and Potts and Niqui. In the current state of experiments, the correctness proofs rely on an axiomatic, non constructive presentation of real numbers.
Tis talk will describe the latest developments in the MPFR library in the last two years, and future plans for the next two years. This is joint work with Vincent Lefèvre, Patrick Pelissier and Laurent Fousse.
TU Darmstadt, FB Mathematik
Exact real number arithmetic has had the reputation of being excessively slow in comparison to standard machine precision floating point. Even in cases where high precisions are not neccessary, real number systems tend to take hundreds of times longer to compute their results.
RealLib is a system that changes this. It uses an approach that treats functions on real numbers as lower-type objects, which allows it to run very close to the computer hardware. As a result, real number computations with RealLib can run nearly as fast as floating point computations with double precision.
One objective of COMP is to make the mathematician feel at home, computing with COMP, even if he doesn't know anything about floating point numbers, programming or computing architectures. If he means ‘Log x', then he should type ‘Log x' - and that should mean the exact same thing as in mathematics.
Straight from the beginning, there is no place for unreliability in COMP. Each answer of the system has to be correct - barring bugs, of course - and no computation shall be left to go on forever.
So COMP gives the user the full responsibility for the data he's providing. For example, if he wants to know the inverse of a number, he should give a lower bound to the number. This is a strong departure from usual practice - but a departure that is expected to have great rewards as the project goes forward towards its goals.
Imperial College London
Most of you will be arriving at Amsterdam Schiphol airport. The easiest way to get to Nijmegen from there is by train. The train station is under the airport (follow the train signs). Take a train to Duivendrecht (so not to Amsterdam Central Station) and change trains here (go one level up) to go in the direction Utrecht. From Duivendrecht there are direct trains to Nijmegen (via Arnhem). You may also take a train to Utrecht and change trains to Nijmegen there.
Especially on Duivendrecht station and on the trains from Schiphol to Duivendrecht be aware of pick-pockets. Keep an eye on your luggage at all times!
The train trip is 1 hour and 30 - 45 minutes.
There is a train planner on the web.
We have good experiences with:
Bisschop Hamerstraat 14
6511 NB Nijmegen
Tel.: +31 (0)24 - 323 35 94
Fax: +31 (0)24 - 323 31 76
Slightly more expensive is:
6511 XR Nijmegen
Tel.: +31 (0)24 - 360 49 70
Fax: +31 (0)24 - 360 71 77
There also is a web page with alternative accomodation.
The workshop will be held at the campus of the Radboud University.
It is located at lecture room 7 (N1004) on the first floor in the science building in the N1-wing.
There will be sign guiding you to the workshop location from the main entrance of the science building.
In case you enjoy walking the campus is 30 minutes walk from the city
To get to the campus by public transport take the train from Nijmegen station to Nijmegen Heyendaal. This train leaves from platform 35, and runs every 11 and 34 minutes past the hour. The train trip will take 3 minutes. From the train station the walk to the workshop locations takes another ten minutes.
There are also bus lines going to the campus. The buses that run through the Heyendaalseweg are lines 1 (direction Molenhoek) and 11 (direction Brakkenstein).
Here is a map of the campus.
page maintained by Bas