[Agda] Oberwolfach Seminar on Mathematics for Scientific Programming

Jeremy.Gibbons at cs.ox.ac.uk Jeremy.Gibbons at cs.ox.ac.uk
Thu Sep 5 15:55:58 CEST 2013

Call for Participation


Mathematisches Forschunginstitut Oberwolfach
24th to 30th November 2013


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.


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)


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


More information about the Agda mailing list