Dr David Binder

My research is on applying theoretical results from type theory, the lambda calculus and logic to the design of programming languages and compilers. In particular, I am interested in bringing the dualities of the sequent calculus and the data/codata duality from their theoretical niche to the mainstream of the PL community. I am also interested in applications of subtyping outside of the realm of object-oriented languages: How can we use subtyping in languages used for verification, and how does this integrate with type inference.  

I am part of the "Programming Languages and Systems (PlaS)" group at the University of Kent.

My main research areas are:

- Data and codata types, pattern and copattern matching

- Classical sequent calculus and control operators

- Intermediate representations

- Functional programming

- Haskell

COMP4106 Computer Systems (Summer term 26)