Miscellanea
Random Stuff I Made
- Together with Peter Lammich, I created a fully verified LLVM implementation of Harvey's multimodular algorithm to compute Bernoulli numbers. Using this, we were the first to compute the 109-th Bernoulli number, breaking the previous world record of 108. It is however worth noting that our implementation is not better or faster than Harvey's (it is actually a bit slower), but it is fully verified.
- Debirdify, a tool that uses the Twitter API to help you find people you follow on Twitter in Mastodon and elsewhere in the Fediverse. Also works for lists, followers, blocked accounts, muted accounts, etc. Now unfortunately defunct since Twitter decided to revoke my API access.
- Cleaned-up versions of my team's winning solutions for the Proof Ground competition at ITP 2019.
- Unofficial SVG versions of the Isabelle logo: isabelle.svg (text as live SVG text) and isabelle_noembed.svg (all text converted to paths).
Personal Interests
- Learning languages, linguistics, and phonetics
- In particular: learning and speaking Esperanto (bonvolu kontakti min se vi volas paroli Esperanton kun mi!)
- Bouldering, climbing, mountaineering, trail running, ski touring
- Playing the accordion and the low whistle
Recommended links
- The website of Isabelle, the Interactive Theorem Prover with which I work
- The free Concrete Semantics book by Nipkow and Klein, which serves as a good introduction to both Isabelle and the subject of programming language semantics
- Another free Isabelle-related textbook, Functional Data Structures and Algorithms. A Proof Assistant Approach by Nipkow et al. This one includes a chapter on median-of-medians selection by me.
- A web cartoon every student should know. And probably everyone who works at a university as well.