Skip to content
Avatar
🦅
I want to apply for a Ph.D.
🦅
I want to apply for a Ph.D.
  • Block or report user

    Block or report ice1000

    Block user

    Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

    Report abuse

    Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

    Report abuse
2.5k followers · 434 following · 551

Highlights

  • Arctic Code Vault Contributor
  • Pro

Organizations

@agda @JuliaEditorSupport @pest-parser @EmmyLua @ice1k @devkt-plugins @owo-lang @arend-lang

Sponsors

@xxchan @li-xin-yi
ice1000/README.md

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

  • 🌱 I have a blog, opensource-contributions, a resume, a research profile, and a codewars profile.
  • 🤔 I'm learning HoTT and is researching on its constructive interpretations, like cubical type theories.
  • 💬 Ask me about IDEs, type theories and implementation of (univalent) dependent type systems!

Pinned

  1. JetBrains/Arend

    The Arend Proof Assistant

    Java 469 21

  2. agda/agda

    Agda is a dependently typed programming language / interactive theorem prover.

    Haskell 1.4k 176

  3. pest-parser/intellij-pest

    pest grammar file support for all JetBrains IDEs

    Kotlin 25 3

  4. agda/cubical

    An experimental library for Cubical Agda

    Agda 217 67

  5. owo-lang/narc-rs

    (WIP) Dependently-typed programming language with Agda style dependent pattern matching

    Rust 52 2

  6. resume

    👾 My resume / 我的简历

    TeX 433 142

2,945 contributions in the last year

Dec Jan Feb Mar Apr May Jun Jul Aug Sep Oct Nov Mon Wed Fri
Learn how we count contributions.
Less
More

Contribution activity

December 2020

Created 20 commits in 5 repositories
Created 1 repository

Created a pull request in hellogcc/OSDT2020 that received 1 comment

Add TIZ's talk

+11 −3 • 1 comment

Seeing something unexpected? Take a look at the GitHub profile guide.

You can’t perform that action at this time.