Please note: This master’s thesis presentation will take place online.
Ende Jin, Master’s candidate
David R. Cheriton School of Computer Science
Supervisors: Professors Yizhou Zhang, Ondřej Lhoták
With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs.