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, same as Idris2!
    • The website contains installation instructions and basic tutorials. Stay tuned for more!
  • Automated theorem proving with Chase Norman.
• 💬 Ask me about IDEs, type theories, implementation of (univalent) dependent type systems, and 3A yoyoing!

Where to find my writings

• (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.

Fun stuffs

• CodeWars

Visit count (since 23 Feb 2023):