Small TYPES workshop

Constructive analysis, types and exact real numbers.

3/4 October 2005

Nijmegen, the Netherlands

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.

Monday, October 3th

09:30-10:30 Norbert Müller(invited speaker) Concepts for implementing exact real arithmetic
10:30 Coffee
11:00-11:30 Branimir Lambov RealLib: an Efficient Implementation of Exact Real Arithmetic
11:30-12:00 Yann Kieffer Introducing the COMP project
12:00 Lunch Kantine
14:00-15:00 Erik Palmgren Constructive problems in elementary homotopy theory
15:00-15:30 Coffee
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
17:00-18:00 Drinks Common room
18:00 Dinner Heertjes

Tuesday, October 4th

09:30-10:30 Martín Escardó (invited speaker) Semantics of programming languages with built-in

abstract data types for exact real numbers
10:30 Coffee
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
12:00-14:00 Lunch Kantine
14:00-14:30 Paul Zimmerman MPFR: recent and future developments
14:30-16:00 Demo session:
Branimir Lambov RealLib
Yann Kieffer First test-drive of COMP
A.A.Kahnban Solving differential equations with imprecise input
16:00-17:30 Drinks common room
17:00-17:30 Presentation of the competition common room
18:00 Dinner Station-Oost

The program of the workshop is still not finalized, and the second day might end later than in the current table.


Martín Escardo, Semantics of programming languages with built-in abstract data types for exact real numbers.

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.

Norbert Müller, Concepts for implementing exact real arithmetic

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.

Branimir Lambov, RealLib: an Efficient Implementation of Exact Real Arithmetic

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.

Yann Kieffer, Introducting the COMP project


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.

Erik Palmgren, Constructive problems in elementary homotopy theory

Department of Mathematics, Uppsala University

We consider the problem of constructivising elementary homotopy theory, and how it may be resolved using fo rmal topology.

Russell O'Connor, An Approch to Fast Real Arithmetic in Coq

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.

Bas Spitters, Almost periodic functions, constructively

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.

Roland Zumkeller, Verification of inequalities over real numbers

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.

Freek Wiedijk, Putting the MathXpert architecture on top of the HOL framework

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.

Yves Bertot, Coinductive implementation of Linear Fractional Transformations

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.

Paul Zimmermann, MPFR: recent and future developments


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.

Branimir Lambov, RealLib: an Efficient Implementation of Exact Real Arithmetic

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.

Yann Kieffer, Introducting the COMP project


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.

A.A. Kahnban, Solving differential equations with imprecise input

Imperial College London

Participants not giving a talk

Prof. D.A. Turner

Iris Loeb

Luis Cruz-Filipe

Jaap van Oosten

Milad Niqui

Benno van den Berg

Peter Aczel

D.V. Paschenik

Dan Synek

Pierre Corbineau

Herman Geuvers

Assia Mahboubi

Ulrich Berger

N.A. Schumacher

Laurent Fousse

Henk Barendregt

Richard B. Kreckel

Chris Heunen

Jasper Stein

Vincent Lefevre


Herman Geuvers Nicole Messink Milad Niqui Bas Spitters Freek Wiedijk

If you want to contact us please do so at

Getting to Nijmegen

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:

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 108-112

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.

Getting to the Workshop

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 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