After graduating from the University of British Columbia (UBC) in Spring 2020, Jonathan Chan continues to pursue his research interests in programming languages (PL) as a master’s student at UBC. His work has resulted in a proof of concept for more robust termination checking in Coq, an interactive proof assistant.

Jonathan initially wanted to focus on physics at UBC, but he discovered his passion for computer science after doing co-op placements. While many of his peers pursued careers in industry after completing co-ops, Jonathan wanted to explore different career paths, motivating him to give research a shot.

Jonathan’s journey to research started in his undergraduate studies with a game of professor telephone. After he excelled in a programming languages course, the course instructor recommended that he talk with another professor about getting involved in PL research. That professor subsequently recommended that he talk with yet another professor, Prof. William Bowman, who ultimately became Jonathan’s advisor. 

With the guidance of Prof. Bowman, Jonathan began working on the proof assistant Coq. Coq provides a formal language to express mathematical definitions, theorems, and algorithms and mechanically checks their proofs. To perform this checking, Coq requires all programs terminate for validity and usability. Currently, Coq checks for termination using methods that examine the syntactic structure of the programs. However, there are other methods to termination checking that are more robust, where termination checking is done as part of type checking. Jonathan’s goal was to implement one of these methods in Coq’s type checker and formally describe his changes to make it practical. Together with a student from the University of Waterloo, Jonathan improved upon his implementation and worked on metatheoretical results — results that formalize the objects, such as expressions and relations, of a theory.

In addition to enjoying the technical aspects of programming languages and disseminating his work, Jonathan also found community through research. He had regular in-person meetings with Prof. Bowman, which was pivotal in advancing his research. He also had opportunities to attend a PL summer school and conference. “I really enjoyed hearing about all the new research other people are doing, being able to share what I was doing, and generally feeling like I was part of a larger community.” Jonathan credits his positive research experiences in undergraduate for shaping his current career path. He was welcomed into Prof. Bowman’s lab and built camaraderie with the lab’s graduate students. “The environment of the lab was part of how I decided to stay at UBC for my Master’s.” 

Outside of the lab, Jonathan is a clarinetist for UBC’s marching band, though that has been put on pause with the current pandemic. He has recently picked up baking as a new hobby to fill quarantine time. While he may no longer be able to have weekly in-person meetings with his advisor, Jonathan continues to explore interesting problems in PL, perhaps with a side of something fresh from the oven.

-Written and edited by Jean Salac