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. My PhD focused on developing a modular treatment of the syntax and semantics of higher-order algebraic effects.

I am about to land in a post-doctoral research position at Imperial College London, but I am also looking for more permanent jobs in academia and industry. Please let me know if you are hiring!

Education

• From 2020 to 2024, I worked with Nicolas Wu in the functional programming group at Imperial College London.

  My focus was the mathematical models of computational effects, in particular, algebraic effects and scoped effects (which are first-order operations that do not commute with substitution). My PhD thesis is Structure and Language of Higher-Order Algebraic Effects.

• 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!

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