David Binder

Type theory, logic and programming languages.

Welcome to my academic website. I am a researcher in type theory, logic and programming languages at the University of Tübingen, where you can find me here. The research topics and areas I am mainly interested in are:

  • Using pure functional programming techniques for solving real problems
  • The duality of data types and codata types, and inductive and coinductive definitions
  • The combination of multiple evaluation strategies within the same language
  • Computational classical logic and the sequent calculus, and the use of the sequent calculus as a compiler intermediate language
  • The theory of subtyping and its applicability to functional languages (as opposed to subtyping in object oriented languages)
  • Logic and proof theoretic semantics, where I also write about the early history of inferentialist meaning theories for logic, especially in the logical writings of Karl Popper