The oi-codes from ice1000

View Code? Open in Web Editor NEW

:closed_lock_with_key: Solutions for online code challenges. Don't be evil.

License: GNU Affero General Public License v3.0

C++ 14.84% C 31.89% Pascal 0.19% Java 9.17% Batchfile 0.01% Kotlin 5.81% Haskell 16.95% Dart 8.37% Shell 0.13% Ruby 0.83% JavaScript 2.78% Go 0.80% Python 0.15% Crystal 0.06% C# 4.99% Rust 2.39% TypeScript 0.31% Elixir 0.01% Clojure 0.01% Brainfuck 0.30%

oi-codes's Introduction

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.