ice1000 Follow

ice1000 Follow

🦅

I want to apply for a Ph.D.

Tesla Ice Zhang‮ ice1000

🦅

I want to apply for a Ph.D.

Penn State | PLT (dependent types, Arend & Agda hacker) | Programming for interest

Follow

2.3k followers · 405 following · 517

@JetBrains
China, Pennsylvania, Gensokyo
Sign in to view email
https://ice1000.org

Highlights

Arctic Code Vault Contributor
Pro

Organizations

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 profile, and a codewars profile.
🤔 I'm learning HoTT and is researching on its constructive interpretations.
💬 Ask me about IDEs, type theories and implementation of dependent type systems!

Pinned

JetBrains/Arend

The Arend Proof Assistant

Java 419 21
agda/agda

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

Haskell 1.3k 165
pest-parser/intellij-pest

pest grammar file support for all JetBrains IDEs

Kotlin 25 3
agda/cubical

An experimental library for Cubical Agda

Agda 186 55
owo-lang/narc-rs

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

Rust 46 2
resume

👾 My resume / 我的简历

TeX 408 142

2,736 contributions in the last year

Activity overview

Contributed to JetBrains/Arend, owo-lang/narc-rs, JetBrains/intellij-arend and 5 other repositories

Contribution activity

July 2020

ice1000/ice1000 Jul 27
ice1000/arend-language-server Kotlin Jul 12
ice1000/vscode-arend TypeScript • Built by Jul 7
ice1000/arend-io Java Jul 4

Created a pull request in JetBrains/intellij-arend that received 1 comment

Support string literals

+22 −4 • 1 comment

Add `length` field to `SourcePosition` Jul 27
Improve position Jul 18
String literals Jul 6

Compile Java with utf-8 Jul 21
Adapt latest literal checker API Jul 14
Workaround github actions, improve build.gradle.kts Jul 4

ci: Remove size-solver from nightly release and script Jul 31

Just some nits Jul 29

Fix incorrect order of clauses in pattern-matching Jul 26

Created an issue in antlr/intellij-plugin-v4 that received 5 comments

Plugin exception

IDE: IC-202.6397.59 OS: Windows 10 2004 Stacktrace: ExternalToolPass: com.intellij.diagnostic.PluginException: annotator: org.antlr.intellij.plugin…

5 comments

Load file on \import in Repl Jul 27
StringIndexOutOfBoundsException Jul 25
Instantiation of inference variables might be too eager Jul 23
Unification enhancement Jul 23
Pattern matching witness, or `proof` keyword in Idris Jul 23
Is that a problem of variable inference? Jul 14
Support `:set +s` in ghci. Jul 11

Support semantic highlighting Jul 27
Use Ctrl+C to interrupt a computation in REPL. Jul 11
Support pure expression highlighting Jul 11
Save history in REPL Jul 11
REPL pretty printing behavior improvements Jul 11

Write about Arend's syntactical homotopy truncation Jul 27
Write about the proof of univalence in HoTT-I Jul 27
Write about the Glue structure in CTT Jul 27
Write about transp and transpX in cubical agda Jul 27

Highlight the `as` part of import statements. Jul 23

Doesn't typecheck in IDE Jul 14

You can’t perform that action at this time.