David Binder
Software Engineering
FB Informatik
Universität Tübingen
Sand 13
72076 Tübingen
Germany

Telephone: +49 - (0) 70 71 - 29 - 70 516
E-Mail: david.binder(at)uni-tuebingen.de
Office: B211
Office hours: by appointment

Personal website

A list of my publications, slides for my presentations and my teaching activities are available on my personal website.

Research Projects

Uroboro

Publications

Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments

by Bohdan Liesnikov, David Binder, and Tim Süberkrüb

In The Art, Science, and Engineering of Programming 10(3), 2025.

Learn More

Grokking the Sequent Calculus (Functional Pearl)

by David Binder, Marco Tzschentke, Marius Müller, and Klaus Ostermann

In Proceedings of the International Conference on Functional Programming (ICFP). ACM Press, 2024.

Learn More

Deriving Dependently-Typed OOP from First Principles

by David Binder, Ingo Skupin, Tim Süberkrüb, and Klaus Ostermann

In Proceedings of the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), 2024.

Learn More

Introduction and Elimination, Left and Right

by Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen

In Proceedings of the International Conference on Functional Programming (ICFP). ACM Press, 2022.

Learn More

Structural Refinement Types

by David Binder, Ingo Skupin, David Läwen, and Klaus Ostermann

In Proceedings of the International Workshop on Type-Driven Development. ACM Press, 2022.

Learn More

Decomposition Diversity with Symmetric Data and Codata

by Klaus Ostermann, Julian Jabs, David Binder, and Ingo Skupin

In Proceedings of Symposium on Principles of Programming Languages (POPL 2020), 2020.

Learn More

Assigned Thesis Topics

Sebastian Voigt

October 5, 2022

Implementing a Monadic Testsuite Driver

Ordinary wisdom says that the individual tests in a testsuite should be independent of each other. That is, each test should be able to run independently of any other test, and in any order. This independence allows the testsuite driver to execute tests in parallel and easily summarize the results using a tests passed / tests failed metric.

Sebastian Voigt

June 8, 2021

Interaktive Lehrbücher

Viele der Lehrmaterialien welche wir in der Lehre verwenden bestehen aus nicht interaktiven Skripten und Foliensätzen. Aber die Inhalte der Informatik, under gerade auch der Programmiersprachentheorie, eignen sich besonders gut für eine interaktive Präsentation. Durch eine interaktive Präsentation können auch sehr abstrakte Inhalte greifbar und verständlich gemacht werden. So wird zum Beispiel häufig auf Animationen und interaktive Graphiken zurückgegriffen, um die Ausführung von Algorithmen zu veranschaulichen. Im Rahmen dieser Bachelorarbeit wollen wir einige unserer Lehrmaterialien um interaktive Elemente ergänzen. Einige konkrete Beispiele die wir gerne umsetzen würden sind:

Sebastian Voigt

August 10, 2020

Supercompilation for Ouroboro

Supercompilation is a compile-time optimization technique which uses partial-evaluation in order to generate an optimzed version of the program. Supercompilation is known to generate significant speedups and to subsume various other optimization techniques. The downsides of supercompilation are potentially huge increases in both compile-time and binary size.

Finished Thesis Topics

Justus Springer

August 10, 2020

Algebraic Subtyping for Ouroboro

Algebraic subtyping is a new approach which unifies parametric polymorphism, subtyping and complete type inference with principal types. The presentations used in the literature illustrate the approach by considering systems with function types, record types and base types, since these form a minimal type theory which allows to illustrate contravariance (function types) and subtyping (record types).

Florian Engel

August 10, 2020

Dependent Data and Codata Types

User-defined data and codata types are two dual and complementary ways to specify types and their inhabitants. Data types specify canonical producers which are built up by constructors, and non-canonical consumers which are formed by pattern matching on constructors. Codata types specify canonical consumers which are built up by destructors, and non-canonical producers which are built up by copattern matching on destructors. For example, using (indexed) codata types it is possible to replace a builtin (dependent) function type by a user defined type.

Florian Engel

September 20, 2018

Implementing the language server protocol for Koka

The Language Server Protocol (LSP) defines a protocol used between an editor or IDE and a language server that provides language features like auto complete, go to definition, find all references etc. The Language Server Protocol has to be implemented once for every programming language and once for every editor, instead of once for every combination of programming language and editor, thus reducing a m x n problem to a m + n problem.

Pavel Karasik

May 30, 2018

Implementing functional graph algorithms in a dependently typed language

In functional languages, such as Haskell, we find existing libraries for working with graphs. These libraries contain the definitions of the necessary datatypes and the functions working on them. Examples of such libraries (in Haskell) are the FGL library by Martin Erwig and the Data.Graph module in the containers package.

News

December 18, 2019

Presentation at the Symposium on Principles of Programming Languages 2020

Ingo Skupin
Ingo Skupin presents the paper Decomposition Diversity with Symmetric Data and Codata at the Symposium on Principles of Programming Languages in New Orleans (USA).