Roland Zumkeller's Web Page

At the moment I'm mostly gardening.

In a former life I used to work in finance, mostly writing programs in Haskell.

In another former life I was a postdoc in Pitt's math department, working on the Flyspeck project. Before then I studied and worked in the TypiCal project at Ecole Polytechnique, and also at the Microsoft Research INRIA Joint Centre, both near Paris. My research interests are formal methods and global optimization.

I've developped optimization methods based on Bernstein polynomials, aiming at a formal verification of the non-linear inequalities occurring in Tom Hales' proof of the Kepler conjecture. A Haskell implementation is available below. The latest changes to it are listed here.

In fall 2009 and spring 2010 I taught MATH 0280: Introduction to Matrices and Linear Algebra.

**Sergei** -
A global optimization tool based on Bernstein polynomials,
written in Haskell.

**Naufrage** -
A tool for sum of squares (S.O.S) decomposition of
polynomials. This highly experimental implementation is in OCaml.

**Texcaml** -
a tool to insert TeX into OCaml comments.

**Cucumber** -
the Coq version of Sergei (outdated).

**A
Revision of the Proof of the Kepler Conjecture** (Thomas Hales,
John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland
Zumkeller) *Discrete
and Computational Geometry*

**Global Optimization in Type Theory** (Roland
Zumkeller) *PhD thesis*

**Formal Global Optimisation with
Taylor Models** (Roland Zumkeller) *Lecture
Notes in Computer Science*

**Formal
Verification of Dynamic Real-Time State-Transition Systems Using
Linear Logic** (長谷部 浩二
, Jean-Pierre Jouannaud, Antoine Kremer, 岡田 光弘,
Roland Zumkeller) *Proceedings of Software
Science Conference, Nagoya*

Open Yale Courses

TSF Jazz

Les arrondissements de Paris

How to make mayonnaise

Persian Poetry

Persian-English dictionary by Franics Joseph Steingass

Digital Photography

New York Review of Books

London Review of Books

Stratfor

Aljazeera English

Cost of War since 2001

Hoogle - find Haskell functions by their type

Detexify - find LaTeX symbols by drawing them

Some photos taken on trips to Iran (April 2006) and to Israel/Palestine (December 2007).

My T'ai Chi master (in Paris).

شتر آهسته می رود، شب و روز.

The camel walks slowly, but by night and day.

(Persian proverb)

email: (first name).(last name)@gmail.com