I am interested in logical and algebraic methods in programming languages. The main theme of my research is designing and analysing formal languages that can be used for describing complex things easily. During my PhD, I have focused on developing a modular treatment of the syntax and semantics of higher-order computational effects.

Education

• From 2020, I am a PhD student of Nicolas Wu in the functional programming group at Imperial College London.

  My focus is the mathematical models of computational effects, in particular, algebraic effects and scoped effects (which are first-order operations that do not commute with substitution).

• From 2017 to 2019, I worked with Josh Ko , Ichiro Hasuo and Zhenjiang Hu as a postgraduate student at the National Institute of Informatics, Japan (joint with SOKENDAI, the Graduate University for Advanced Studies) and obtained a Master of Informatics.

  In this period I studied techniques to do equational reasoning about programs manipulating data structures based on pointers (which my Master's thesis is about). Also, I worked with Zirun Zhu and Josh on formalising stronger lens properties called retentive lenses in the context of bidirectional transformations.

• From 2013 to 2017, I did my Bachelor of Science at Peking University where I majored in computer science and technology.

  Here Yingfei Xiong introduced me to programming language theory, which I immediately took as the subject that I would spend my career on. I also worked on distributional word representations for a while.

Employment

• During 2019–2020, I worked as a software engineer for Sourcebrella, Inc, a start-up company making commercial static program analysers, founded by Xiao Xiao.

My name Zhixuan, which is the pinyin transcription of Chinese '至轩', is mysterious for non-Chinese speakers. An approximation of its pronunciation is gee-shaun, but I am happy with whichever way people pronounce it, so don't let it be an obstacle if you want to talk to me! (If you are interested in the exact pronunciation, you can try command say -v Ting-Ting '至轩' to hear it if you are using a Mac.)

I have recently started writing down more notes about my thoughts using Forester. Currently there is only one unfinished note on Synthetic Tait Computability.