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)!
-
(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.
- CodeWars
- Visit count (since 23 Feb 2023):