Topics on My New Hugo Site

Choreographic Programming

Mon, 01 Jan 0001 00:00:00 +0000

Write a whole distributed system as one script, and let the compiler split it up.

A distributed system is normally written as many separate programs, one per participant, which have to agree on a protocol that exists nowhere in the code. Choreographic programming writes the interaction once, as a single program that names every participant, and a compiler projects it onto the individual endpoints. Protocol mismatches and whole classes of deadlock become programs you cannot write in the first place.

Array & Differentiable Programming

Mon, 01 Jan 0001 00:00:00 +0000

← Back to Home

Compilers for machine learning: derive and prove what ML frameworks hard-code.

Machine learning runs on a small set of operations (multiply these arrays, differentiate this, invert that) that a compiler ought to derive rather than have a human write out by hand. My work gives these transformations a functional foundation, so they can be optimized aggressively and proved correct rather than trusted.

Arrays: a normal form for array programs in which partial evaluation and common subexpression elimination become one algorithm (ECOOP'24).
Derivatives: automatic differentiation optimized by rewrite strategies, with Timon Böhler (FTfJP'23).
Inverses: a verified search for inverse functions, applied to normalizing flows, with Timon Böhler and Benedict Smit (preprint).

Highlight

🏅 Distinguished Paper Compiling with Arrays, ECOOP 2024

Collaborators

Timon Böhler Jannis Brugger Mattia Cerrato Cedric Derstroff Stefan Kramer Daniel Maninger Mira Mezini Viktor Pfanschilling Benedict Smit Pascal Weisenburger

Timeline

2023FTfJP @ ECOOP · Short paper

Using Rewrite Strategies for Efficient Functional Automatic Differentiation

Timon Böhler, David Richter, Mira Mezini

Incremental & Reactive Programming

Mon, 01 Jan 0001 00:00:00 +0000

← Back to Home

Compilers that turn plain functional code into computations that redo only what changed.

Most programs throw away their own work: change one cell of a matrix or one row of a table, and the whole computation runs again from scratch. Incremental programming derives from an ordinary functional program a second one that maps a change to the input to the corresponding change to the output, reusing everything that was already computed.

Effects & Type Theory

Mon, 01 Jan 0001 00:00:00 +0000

← Back to Home

Notations and type checkers that let programmers write what they mean, and still check it.

A type system is a negotiation. The programmer wants to write what they mean; the compiler wants a guarantee it can actually check. Push too hard on the guarantee and the notation turns rigid (effects marshalled one per line, motives spelled out by hand). Push too hard on convenience and the guarantee evaporates. My work tries to move that boundary rather than pick a side: