I like tools for organising my own reasoning. As a research-oriented programmer, I look for mathematical and logical structures of computation that can help me to understand and develop correct programs, and expressive programming languages where such structures can be made explicit. I approach programming problems mainly from the perspective of intuitionistic type theory, which substantially overlaps with functional programming. For theoretic modelling, my weapon of choice is Agda; for practical programming, I use Haskell.

I believe that two features of type theory make it a useful tool for programming: (i) an expressive language of types for precise specification, abstraction, and modularisation, and (ii) formal and conceptual combination of programs and proofs. My research has been driven towards developing theories and applications to explain and demonstrate how the two features are useful.

See my personal website for more detail.