Tesla Zhang

I am a third-year Ph.D. student in the Computer Science Department at CMU, advised by Professor Stephanie Balzer. My research is about logical relations for session type theories and mechanization of these logical relation proofs.

My personal interests include implementing type checkers for dependent type theories, making fancy programming language tools, programming language design, and thinking about type theories from a category theoretical point of view.

Some links: ORCiD, GitHub, arXiv, Aya Prover.

I spend my spare time developing the Aya Prover and play yoyo.

• My email is teslaz [at] cmu [dot] edu.
• My office is in the Gates–Hillman Center, floor 5, 5103 (need ID access outside business hours).

• Chase Norman: automated theorem proving for dependent type theories (online demo).

This website is under construction, stay tuned!