Tao Xue's Homepage

Tao Xue

Room 225 , McConnell Engineering Building
3480 University Street
School of Computer Science,
McGill University
Montreal, Quebec, Canada
H3A 0E9
Email: taoxue@cs.mcgill.ca

About me

I'm now working as a postdoc fellow in the CompLogic Group in School of Computer Science, McGill University with professor Brigitte Pientka. I was a Ph.D student at Department of Computer Science, Royal Holloway University of London, studied with professor Zhaohui Luo. Before that, I did my undergraduate study at Peking University and master at State Key Laboratory of Computer Science, Institutue of Software, Chinese Academy of Science


Generally, I'm interested in logics, type theory, theorem proving and functional programming language.

Beluga is a functional programming with higher-order abstract syntax based on contextual modal type theory. It is an environment for programming with and reasoning about deductive systems.
  • I'm participating in extending Beluga's framework with features like termination checking and polymorphism.
  • I'm also looking into using Beluga as a language for proof-carrying authorization.

  • During my PhD, I worked mainly on coercive subtyping. I amended the framework of coercive subtyping and studied the relation between a type system and its coercive subtyping extension. I also did some work on using type theory with coercive subtyping in linguist semantics interpretation.