Projects

Demo: Image Compression with SVD

Singular value decomposition is an important matrix factorisation. It can be used to approximate a matrix by a matrix of lower rank, which can be stored and processed more efficiently. This interactive webpage allows the user to compress images (which can be regarded as combination of three matrices, one for each color channel) using SVD and see how the quality of the compressed image depends on the number of singular values.

visualization math react

Operational Transformation

OT is the synchronization algorithm used in many real-time collaborative applications like Etherpad and Google Docs. It is based on a transform function for merging concurrent changes. I've implemented a family of OT libraries in several programming languages, wich include a transform function for text documents and client/server modules. I have also created an interactive visualization, which helps understanding OT.

haskell visualization algorithms d3

quantities

A library for type-safe physical computations in the dependently typed programming language Idris. It makes unit errors impossible by tagging each float that represents a physical measurement with its unit. A value can be converted from one unit to another unit provided that the units have the same quantity (e.g. area). To ensure this at compile time, units are indexed by their quantity. The library uses the observation that both units and quantities are a free abelian group and the existence of a natural group homomorphism φ : Units → Quantities.

idris api-design

diagrams-rubiks-cube

This library draws Rubik's Cubes using diagrams. Given a start (or end state) and a series of steps to follow, it can produce images like the one on the right. I used Edward Kmett's lens library to succinctly express the calculation of the new facets after a rotation. I used this library to generate the images for this solution guide.

haskell math writing

Purely Functional Data Structures in Idris

Implementations of various functional data structures from Okasaki's book and elsewhere in the dependently typed programming language Idris. Where possible, I tried to use size-indices. All implementations have been verified as total by the Idris compiler.

idris algorithms

uni-spicker

Cheat sheets which I'm writing to prepare for exams and as a reference for later. All together, they comprise over 150 pages of dense mathematics and computer science!

latex math writing

Curry Club Augsburg

I designed the logo and website for the local Haskell/FP user group which I have co-founded.

webdesign hakyll

Halma

I implemented the game rules and a simple diagrams-based GUI for my favorite board game. A friend of mine wrote a simple AI using search trees, which is actually quite hard to beat!

haskell

Open Source Contributions

reroute

This library implements the routing in the Spock Haskell web framework. It uses type-level lists to index routes by thy types of their parameters. I've implemented it together with Alexander Thiemann, the author of Spock, during HacBerlin2014. I've also written a tutorial on the new routing system for the Spock blog.

haskell api-design writing

Timsort

I contributed an implementation of my favorite sorting algorithm to vector-algorithms. The great thing about Timsort is ~~its name~~ that it is very fast (meaning linear time) on data that is already (partially) sorted.

haskell algorithms

engine-io

This Haskell library by Oliver Charles provides the server component for engine-io, a protocol providing a socket-like communication channel between web clients and servers. I wrote the engine-io-yesod backend. I'm also a co-maintainer of the library.