Roland Zumkeller's web page
In a 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.
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).
Global Optimization in Type Theory (Roland Zumkeller) PhD thesis
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
Les arrondissements de Paris
How to make mayonnaise
Persian-English dictionary by Franics Joseph Steingass
New York Review of Books
London Review of Books
Cost of War since 2001
Hoogle - find Haskell functions by their type
Detexify - find LaTeX symbols by drawing them
My T'ai Chi master (in Paris).
شتر آهسته می رود، شب و روز.
The camel walks slowly, but by night and day.
email: (first name).(last name)@gmail.com