I am interested in the discovery of mathematical and logical structures of computation so that they can be manifested in programming languages and effectively guide the programmer. I approach problems mainly from the perspective of intuitionistic type theory or, in general, functional programming. For theoretic modelling, my weapon of choice is Agda; for practical programming, I use Haskell.

I have been exploring the potential of dependently typed programming, where sophisticated correctness properties and proofs can be integrated into types and programs, and mechanically verified by type-checking. More interestingly, with an interactive development environment (like the Emacs mode offered by Agda) that provides semantic hints in the form of type information, the programmer can gain better “situation awareness” regarding the meaning of the program being constructed. This is made possible primarily because of inductive families, and my DPhil thesis developed datatype-generic techniques for improving usability and reusability of inductive families. I also studied the Algebra of Programming (a.k.a. Bird–Meertens formalism or program calculation) and contributed to its dependently typed formalisation.

I have also worked on bidirectional transformations for solving consistency maintenance (synchronisation) problems. More specifically, my focus was on bidirectional programming, which is largely synonymous with the construction of lenses. My main results in this area were built around a small “putback-based” bidirectional programming language BiGUL (Bidirectional Generic Update Language), about which there were an Agda formalisation, a Haskell port, and an axiomatic semantics that helps to explain how to think about bidirectional programs unidirectionally.