Programming Languages

David Binder, M.Sc.

Photo of David Binder

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

+49 - (0) 70 71 - 29 - 70 516
+49 - (0) 70 71 - 29 - 50 82
Office hours
by appointment

Research Projects



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

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.

Read more ...

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

Read more ...

Assigned Thesis Topics

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

Read more ...

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.

Read more ...

Finished Thesis Topics

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.

Read more ...

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.

Read more ...


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

Read more ...