David Binder

Dr David Binder's research is on applying theoretical results from type theory, the lambda calculus and logic to the design of programming languages and compilers. In particular, he is 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. He is 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.  

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

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