The Coq mailing list

[Jeremy.Gibbons AT cs.ox.ac.uk]

Call for Participation

OBERWOLFACH SEMINAR ON 
MATHEMATICS FOR SCIENTIFIC COMPUTATION

Mathematisches Forschunginstitut Oberwolfach
24th to 30th November 2013
http://www.mfo.de/occasion/1348a


MOTIVATION

Computational science today depends crucially on simulations, which are 
typically based on algorithms that have a sound mathematical justification.  
For example, an iterative procedure such as Newton's method is motivated by 
appealing to the properties of twice continuously differentiable functions 
and their Taylor expansion, which also yield convergence conditions and 
approximation estimates.

These algorithms are then implemented on a computer, using a programming 
language such as Fortran or C++.  Often, the implementation will introduce 
new computational steps and otherwise modify the structure of the 
mathematical algorithm - for handling or reducing round-off errors, enabling 
more efficient memory access, exploiting parallelization, and so on.  As a 
result, the final implementation usually looks very different from the 
mathematical algorithm, and the justification given for the latter does not 
directly extend to the former.  But if we are to ensure the correctness of 
simulations, we need mathematical certainty for both.

We aim to bring to the scientific programming community mathematical 
techniques that allow us to achieve the transition from mathematical 
algorithm to efficient implementation in a principled manner, with each step 
motivated by the application of a mathematical theorem. The intended 
participants are students and researchers in computational science (including 
areas such as engineering, biology, and economics), and any scientists 
dissatisfied with state of the art in transforming mathematics into code. 
They will be equipped subsequently to make a significant contribution to 
increasing the correctness of the simulations that play such an important 
role in current scientific activity.


CONTENT

This rigorous approach to programming is most easily presented in the 
framework of functional programming: program calculation can be reduced to 
straightforward equational reasoning, provided that all program variables are 
immutable.  Accordingly, we will introduce the basic syntax and ideas using 
Haskell, currently the one of the most successful functional programming 
languages.  The emphasis is not on functional programming as such, and even 
less so on a specific language such as Haskell; but rather, on the 
mathematics behind program development, which can then be transferred to 
other contexts, such as imperative programming, or parallel programming.

This mathematical foundation lies in category theory, which unifies what 
could otherwise appear as a large collection of "bite-sized" theorems for 
program development, too many for any developer to remember and use 
efficiently.  Category theory is a broad subject: we will limit ourselves to 
what is essential as a framework for datatypes and programs (functors, 
universal properties, algebras, monads). The many examples, such as fusion 
(loop elimination), optimal bracketing (important for non-associative 
operations such as those on floating-point numbers), or parallel programming 
skeletons (such as Google's MapReduce), will be readily understandable and 
relevant to scientific computing practitioners.

One of the most effective ways to counter floating-point errors and to obtain 
validated results is to use interval analysis, which however requires more 
complex data structures and algorithms than is common in other areas of 
scientific computation.  Extending a function on real or floating-point 
numbers to one on intervals is a matter of symbolic computation, similar to 
the symbolic differentiation or integration that is performed by tools such 
as Mathematica.  The problem of obtaining the best extension is complicated 
by the fact that some familiar properties (such as that x-x=0 for any x, and 
distributivity of multiplication over addition) do not apply to intervals, 
and is a good source of examples for calculational programming.

Finally, we will present a larger application, a generic program for 
inter-temporal optimization with dynamic programming.  This kind of problem 
is ubiquitous in economic modeling, and hence in many integrated assessment 
models, such as those aiming to compute costs of climate change. It has both 
algebraic aspects (the organization of the computation for backward 
induction), which can be tackled with the categorical methods presented, and 
numerical ones (the local optimization techniques), where interval analysis 
can be used.

The Seminar is organized by:

* Paul Flondor, Professor of Mathematics at Politehnica University Bucharest
  
(pflondor AT yahoo.co.uk)
* Jeremy Gibbons, Professor of Computing at the University of Oxford
  
(jeremy.gibbons AT cs.ox.ac.uk)
* Cezar Ionescu, researcher at Potsdam Institute for Climate Impact Research
  
(ionescu AT pik-potsdam.de)


HOW TO APPLY

Applications to participate should include

* full name and address, including e-mail address
* short CV, present position, university
* name of supervisor of PhD thesis
* a short summary of previous work and interest

and should be sent preferably by e-mail (pdf files) to:

  Prof. Dr. Dietmar Kröner
  Mathematisches Forschungsinstitut Oberwolfach
  Schwarzwaldstr. 9-11
  77709 Oberwolfach-Walke
  Germany
  
seminars AT mfo.de

The deadline for applications is 15th September, and the number of 
participants is restricted to 25. The Institute covers accommodation and 
food; thanks to support from the Carl Friedrich von Siemens Foundation, some 
contribution may also be made towards travel expenses. For more information, 
contact the organizers or see the Institute's webpage:

  http://www.mfo.de/scientific-programme/meetings/oberwolfach-seminars