home

teaching

(pre)prints

talks

cv

\lambda

impressum

implementation/formalisation of research work

• Lower bounds for amenable multiplicity
  (Partial) implementation in Lean of results from DOI 10.4171/LEM/66-1/2-8 / arXiv:1910.11716 [math.AT] and arXiv:2202.05606 [math.AT]
  
  
• Finite functorial semi-norms and representability
  (Partial) implementation in Lean of results from DOI 10.1093/imrn/rnv250 / arXiv:1404.6557 [math.AT]
  
  
• L^2-Betti numbers and computability of reals
  Joint work with Matthias Uschold
  (Partial) implementation in Lean of results from 2202.03159 [math.GR]
  
  
• lallop
  Joint work with Nicolaus Heuer
  Implementation of lallop in MATLAB
  Implementation of lallop in Haskell
  This is related to 1911.02470 [math.GT]
  

implementation/formalisation of teaching material

• Quasimorphisms (2022)
  Basic definitions and properties; more theory/examples will be added! In Lean:
  git repository
  
  
• Quasi-isometries (2022)
  Basic definitions of quasi-isometric embeddings, quasi-isometries, and an alternative characterisation of quasi-isometries; in Lean:
  source code: quasiisometry.lean
  additional files: leanpkg.toml leanpkg.path LICENSE.txt
  
  
• A short introduction to formalising Mathematics in Lean (2022)
  Lecture notes, examples, and exercises are available on the course homepage.
  Extended version: Exploring Formalisation
  
  
• Mini geometry (2021)
  Formalisation (in Lean) of the independence of the parallel postulate in Mini Geometry: src
  
  
• Ergodic theory of groups (2020)
  Formalisation (in Isabelle) of fragments of the theory are available on the course homepage.
  

astrds: an incomplete 2d space game

astrds is an intentionally incomplete 2d space game written in Haskell. The code is intended to be a playground for Haskell programmers who want to add their own features and extensions. The implementation is based on SDL and OpenGL and includes simple audio and joystick support.

Source code (Cabal source package): download at hackage.haskell.org

Screenshots:

Tenth ICFP Programming Contest

I was a member of the organising team of the Tenth ICFP Programming Contest . The prequel can be followed in this blog . Thanks to all the people who tried to morph and save Endo!

Eelco Dolstra, Jur Hage, Bastiaan Heeren, Stefan Holdermans, Johan Jeu\-ring, Andres L\"oh, Arie Middelkoop, Alexey Rodriguez, John van Schie, Clara L\"oh.
Morph Endo! Report on the Tenth Interstellar Contest on Fuun Programming .
© ACM, 2008. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in James Hook and Peter Thiemann, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, Victoria, BC, Canada, September 22–24, 2008, pages 397–408, http://doi.acm.org/10.1145/1411204.1411259.

\Lambda ...

I designed a Lambda cartoon character, living in the universe of functional programming. For example, I created the drawings in the thesis of Andres Löh.