Hello! My name is Jonathan (sometimes Jon; never with an h). I am a Master’s student in the Software Practices Lab at UBC. My research interests include dependent types, proof assistants, type theory, compilers, and mathematical logic.


I worked with Prof. William J. Bowman on my undergraduate thesis on sized types, which is a type-based method of checking termination of recursive functions on (co)inductive data. An implementation in Coq’s kernel can be found on GitHub. I continue to work with him as a Master’s student on type-preserving closure conversion of recursive functions, which will also make use of sized types.


I have been a graduate TA for two courses at UBC: CPSC 311 (Definition of Programing Languages) in 2020WT1 and 2021WT1, where students learn about various features of PLs and write interpreters for them, and CPSC 312 (Functional and Logic Programming) in 2020WT2, where students get some hands-on experience using Haskell and Prolog. I have also been a student volunteer at POPL 2020, ICFP 2020, and POPL 2021, as well as an attendee at PLISS 2019 and OPLSS 2021.

Fun Facts

GitHub button @ionathanch GitLab button @ionathanch Twitter button @ionathanch Mastodon button @ionchy@types.pl Keybase button @ionathan