Tesla Zhang‮ ice1000

Hi there 👋 I go by Tesla Zhang. Typical social media usernames include ice1000 or tizusa.

🌱 I have a personal website, where my resume is also hosted.
👨‍💻 I'm currently working on:
- Session type research with my advisor Stephanie Balzer.
- The Aya language with some interesting ideas. Goal: make it practical, like Idris2, but with effective quotients and constructive proof of funExt!
  - The website contains installation instructions and basic tutorials. Stay tuned for more!
- Automated theorem proving with Chase Norman. Project Demo.
💬 Ask me about IDEs, type theories, implementation of (univalent) dependent type systems, and 3A yoyoing (string tricks using two yoyos)!

Where to find my writings

(graduate, English) Some academic articles are uploaded to arXiv and my research blog.
(late college & graduate, English) Proof assistants related Q&A on Stack Exchange.
(graduate, 中文) Chenjing Bu is building Banana Space (香蕉空间), a modern math wiki in Chinese. I mainly contribute to type theory stuffs and related areas inspired from another contributor Trebor.

如果您想要学习类型论，且对阅读英语感到困难，我非常推荐您浏览香蕉空间的相关板块，这些内容主要面向有一定数学背景的读者。如果您对其中的内容有疑问，请联系我。
(late college, 中文) Basic type theory tutorials & guides on 茶饭.
(mid & late college, English) Thoughts / tutorials about Agda, cubical, and PL design on the Aya website.
(pre & early college, 中文) Loads of low-quality contents, those can be found on 知乎 and my old blog (deleted). I strongly discourage anyone to read them -- unless you explicitly intend to humiliate me.