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:3010:30  Norbert Müller(invited speaker)  Concepts for implementing exact real arithmetic  
10:30  Coffee  
11:0011:30  Branimir Lambov  RealLib: an Efficient Implementation of Exact Real Arithmetic  
11:3012:00  Yann Kieffer  Introducing the COMP project  
12:00  Lunch  Kantine  
14:0015:00  Erik Palmgren  Constructive problems in elementary homotopy theory  
15:0015:30  Coffee  
15:3016:00  Freek Wiedijk  Putting the MathXpert architecture on top of the HOL framework  
16:0016:30  Bas Spitters  Almost periodic functions, constructively  
16:3017:00  Yves Bertot  Coinductive implementation of Linear Fractional Transformations  
17:0018:00  Drinks  Common room  
18:00  Dinner  Heertjes 
09:3010:30  Martín Escardó (invited speaker)  Semantics of programming languages with builtin abstract data types for exact real numbers 

10:30  Coffee  
11:0011:30  Roland Zumkeller  Verification of inequalities over real numbers  
11:3012:00  Russell O'Connor  An Approach to Fast Real Arithmetic in Coq  
12:0014:00  Lunch  Kantine  
14:0014:30  Paul Zimmerman  MPFR: recent and future developments  
14:3016:00  Demo session:  
Branimir Lambov  RealLib  
Yann Kieffer  First testdrive of COMP  
A.A.Kahnban  Solving differential equations with imprecise input  
16:0017:30  Drinks  common room  
17:0017:30  Presentation of the competition  common room  
18:00  Dinner  StationOost 
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 realnumbers, 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
nondeterminism, 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. Multivalued 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.
LeibnizIMAG
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 CCorn 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 CCorn 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 branchandbound 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 MathXpertstyle ‘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.
INRIA Lorraine/LORIA
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 lowertype 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.
LeibnizIMAG
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
N.A. Schumacher
Jasper Stein
Herman Geuvers Nicole Messink Milad
Niqui Bas Spitters Freek
Wiedijk
If you want to contact us please do so at typesreal@cs.ru.nl
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 pickpockets. 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:
Hotel Apollo
Bisschop Hamerstraat 14
6511
NB Nijmegen
Tel.: +31 (0)24  323 35 94
Fax: +31 (0)24
 323 31 76
Slightly more expensive is:
Hotel Courage
Waalkade 108112
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 N1wing.
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
center.
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