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:
- 💬 Ask me about IDEs, type theories, implementation of (univalent) dependent type systems, and 3A yoyoing!
-
(graduate, English) Some academic articles are uploaded to arXiv and my research blog.
-
(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 and late college, English) Thoughts / tutorials about Agda, cubical, and PL design on the Aya website.
-
(pre and 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.
Visit count (since 23 Feb 2023):