David Binder, M.Sc.

David Binder
Universität Tübingen
WSI - Programmiersprachen
Sand 13
72076 Tübingen
Germany

Telephone: +49 - (0) 70 71 - 29 - 70 516
Telefax: +49 - (0) 70 71 - 29 - 50 82
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

Grokking the Sequent Calculus (Functional Pearl)

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

In Proc. Int’l Conf. Functional Programming (ICFP). ACM Press, 2024.

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

Open Thesis Topics

June 20

An Online Repository for Haskell Code Snippets

The idea of fragment-based code distribution is to distribute code in units of individual functions instead of packages as is mostly done today. We have a prototype implementation of a fragment-based code package manager fragnix [0] for Haskell. In a talk at Haskell Implementors Workshop 2017 we gave a demo of how functions could be stored online and retrieved individually [1].

Assigned Thesis Topics

October 5

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.

June 8

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:

August 10

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

August 10

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).

August 10

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.

September 20

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.

May 30

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

Presentation at the Symposium on Principles of Programming Languages 2020

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