Tao Xue's Homepage
Room 225 , McConnell Engineering Building
3480 University Street
School of Computer Science,
Montreal, Quebec, Canada
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.
Tao Xue. Definitional extension in type theory. Accepted by TYPES2013-postproceeding. 2014. [ pdf ]
Zhaohui Luo, Sergei Solviev and Tao Xue. Coercive subtyping: theory and implementation. Information and Computation, Volume 223, February, 2013. pp. 18-42 [pdf]
Tao Xue and Zhaohui Luo. Dot-types and their implementation. Logical Aspect of Computational Linguistics 2012. Lecture Notes of Computer Science vol.7351, pp. 234-249, Springer, 2012. [pdf]
Tao Xue and Qichao Xuan. Proof Search and Counter Model of Positive Minimal Predicate Logic. Electronic Notes in Theoretical Computer Science, 212. pp. 87-102, 2008.[pdf]
Tao Xue. Theory and Implementation of Coercive Subtyping. PhD thesis, Royal Holloway, University of London, 2013. [pdf]
Talk at LACL 2012. Dot-types and their implementation. Nantes, France, July 2012. [slides]
Draf with Zhaohui Luo and Robin Adam. Conservativity of coercive subtyping. 2011. [pdf]
Talk at TYPES 2010. Contextual coercive subtyping. Warsaw, Poland, October 2010. [slides]