Nijmegen, the Netherlands

The workshop will be held at the campus of the Radboud University Nijmegen

The workshop will be held on 6th of October.

12:00-13:00 | Lunch | De Refter | |

13:00-14:00 | Helmut Schwichtenberg) | Simultaneous inductive/coinductive definition of continuous functions | |

14:00-15:00 | Norbert Mueller) | Enhancing imperative exact real arithmetic with functions and logic | |

15:00-15:30 | Coffee |
||

15:30-16:30 | Russell O'Connor | How to Understand What Classical Mathematicians Say | |

16:30-17:30 | John Harrison) | Decidability and undecidability in theories of real vector spaces | |

17:30-18:30 | Drinks |
||

19:00 | Dinner |
Vurrukkuluk |

Vurrukkulluk

*How to Understand What Classical Mathematicians Say*

Usually people consider constructive mathematics as a restriction of classical mathematics where the law of the excluded middle is disallowed. However, I believe that constructive mathematics is better as an extension of classical mathematics which adds constructive existential quantifier and a constructive function space.

In my talk will cover

- How to interpret classical mathematics in a fragment of constructive mathematics.
- How this classical fragment is useful when developing constructive analysis.
- Why classical mathematicians want to increase their expressiveness by adding the constructive existential quantifier to their language.
- Why constructive mathematics is helpful language for computer scientists who want to prove programs correct.

*Enhancing imperative exact real arithmetic with functions and logic*

In the near past, there have been many approaches to `implement' constructive analysis, many of them with the use of functional programmig languages. In this paper we present a similar approach based on the iRRAM-package which has been acknowledged as a fast package for exact real arithmetic in C++. A major concern here is the reduction of space requirements for computations with real numbers.

*Simultaneous inductive/coinductive definition of continuous functions*

When extracting computational content from proofs in constructive analysis it can be helpful to use simultaneous inductive/coinductive definitons of the real numbers and of (uniformly) continuous real functions. The talk reports on an attempt to design the underlying theory, based on recent work of Ulrich Berger.

Decidability and undecidability in theories of real vector spaces

The known decidability of various elementary theories of real numbers
leads to practical decision procedures that are genuinely useful in
formal proofs. Linear real arithmetic is a staple of verification
systems, and recently there has been increasing interest in the
automation of nonlinear arithmetic via various techniques (quantifier
elimination, sum-of-squares decomposition or more heuristic means).

For many purposes, particularly in geometry, it's natural to wonder
whether these results can be extended to analogous theories of real
vector spaces, formulated in a 2-sorted first-order language with a
sort for vectors and another for real numbers. In joint work, Solovay,
Arthan and the speaker have systematically surveyed various theories
of this kind. It turns out that the theories of vector spaces and
inner product spaces are decidable and even admit quantifier
elimination in a suitably expanded language, whereas similar-looking
theories of normed spaces are spectacularly undecidable, at least as
difficult as second-order arithmetic. The universal "linear" theory
of normed spaces, however, is fairly efficiently decidable, and a
decision procedure for this theory has been found to be very useful.

Herman Geuvers Nicole Messink Bas Spitters.

Please contact Nicole Messink for practical matters.

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. Just check the screens.

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.

The workshop will be held at

Gymnasion.

It is located at lecture room GN2.

In case you enjoy walking the campus is 30 minutes walk from the city
center.

There is a bus going to the campus. The buses that run through the Heyendaalseweg are lines 1 (direction Molenhoek) and 11 (direction Brakkenstein), 10 (Heyendael Shuttle), 3,4 (Wijchen via Noord/Zuid) all stop outside the "Bloedbank" opposite our building.

page maintained by Bas