Tesla (Yinsen) Ice Zhang

Research Interests

I work with programming languages, their type systems and underlying type theories. Specifically, the design and implementation of dependent type systems and their applications in the univalent foundations of mathematics.

Apart from that, I am also interested in the design and implementation of Integrated Development Environments (aka IDEs) and their plugins.

My choice of programming languages are Rust, Arend (developer, also develop intellij-arend), Agda (contributor, also contribute cubical-lib), Perl, Kotlin, Java and Haskell.




Toy programming languages implemented by me (> 80% contribution), all dependently-typed.

Some interesting programming language tools:

The best way to understand type theory is to implement it!

Anders Mörtberg