Computer Science
Profile Activity
Meta user
Network profile
856
reputation
5
31

ice1000

I'm into univalent type systems. Worked on Agda and Arend, looking for PhD or similar research position.

Profile: https://personal.psu.edu/yqz5714

5
answers
19
questions
~10k
people reached

Communities (22)

Top Meta Posts
1
0

Top network posts

Top tags (29)

Score 4
Posts 3
Posts % 12
Score 4
Posts 2
Score 4
Posts 2
Score 3
Posts 3
Score 3
Posts 3
Score 3
Posts 2
View all tags →

Top posts (24)

All Questions Answers
Votes Newest
7 What should we return when pattern matching on a Path constructor? Jan 20 '19
6 In Agda's GADT, are “parameterized” and “indexed” different semantically? Oct 12 '18
5 What does it mean if we disable K-rule in Agda? Oct 9 '18
5 Is there really a $ O(1/n) $ algorithm? Nov 30 '17
4 What does “Kan” mean in “Kan operations”? May 14 '19
4 How was Idris' `rewrite` implemented? Nov 26 '17
4 Why cannot match $ Bool \equiv Bool $ with $ refl $ while $1 \equiv 1$ can? Oct 11 '18
4 Can we add dependent type into an existing imperative programming language? Nov 28 '17
4 How was Idris' `rewrite` implemented? Nov 27 '17
4 Fastest way to search a word in a word list? Apr 7 '18
View all questions and answers →

Badges (36)

Gold

—

Silver

5

Rarest

Bronze

31

Rarest

View all badges →

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.