Tesla (Yinsen) Ice Zhang

ORCID iD iconhttps://orcid.org/0000-0002-9050-846X

Research Interests

I work with programming languages, their type theories, and semantics. Specifically, the design and implementation of dependent type systems and their applications in the univalent foundations of mathematics. I want to improve type theories by developing useful types with good computational properties.

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.

I’m developing Aya, a practical proof assistant which features in generalization of definitional equalities and overlapping but confluent pattern matching. It also has some homotopy type theoretical features similar to Arend.




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