Tesla (Yinsen) Ice Zhang

Research Interests

I work with programming languages and their type systems. Specifically, the design and implementation of dependent type systems and their applications in the univalent foundations of mathematics. My choice of programming languages are Rust, Arend (developer), Agda (contributor), Perl, Kotlin and Haskell.

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



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

Some interesting tools:

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

Anders Mörtberg