ºÚÁϳԹÏ×ÊÔ´

My research is currently focussed on dependent type theory.

(à la Martin-Löf) seeks to be a foundation for formal reasoning in mathematics and computer science. Its powerful concept of introduction, elimination and computation rules has proven a robust and extensible way of organising formal reasoning. (initiated by the late Vladimir Voevodsky) is a recently developed flavour of dependent type theory – where higher dimensional mathematical objects reside as first-class objects.

My contributions to the field includes a . Further more, I have contributed to the theory of containers, a model of data structures in type theory, by extending the notion to .