David Binder

Type theory, logic and programming languages.

Welcome to my academic website. I am a lecturer at the University of Kent, where you can find me here, and have previously been at the University of Tübingen, where you can find me here. I am a researcher in type theory and programming languages and mainly interested in the following research topics:

  • 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