Computer Science
user avatar
user avatar
user avatar
ice1000
  • Member for 4 years, 6 months
  • Last seen this week
Profile Activity
Stats
888
reputation
12k
reached
5
answers
19
questions
Communities
View all
About

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

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

Badges
View all badges
This user doesn’t have any gold badges yet.
6
silver badges
32
bronze badges
Top tags
View all tags
5
Score
3
Posts
12
Posts %
4
Score
2
Posts
8
Posts %
4
Score
2
Posts
8
Posts %
3
Score
3
Posts
12
Posts %
3
Score
3
Posts
12
Posts %
3
Score
2
Posts
8
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
question
7
In Agda's GADT, are "parameterized" and "indexed" different semantically?
Oct 12, 2018
question
7
What should we return when pattern matching on a Path constructor?
Jan 20, 2019
question
5
What does it mean if we disable K-rule in Agda?
Oct 9, 2018
question
5
Is there really a $ O(1/n) $ algorithm?
Nov 30, 2017
question
4
Can we add dependent type into an existing imperative programming language?
Nov 28, 2017
question
4
How was Idris' `rewrite` implemented?
Nov 26, 2017
question
4
Why cannot match $ Bool \equiv Bool $ with $ refl $ while $1 \equiv 1$ can?
Oct 11, 2018
question
4
What does "Kan" mean in "Kan operations"?
May 14, 2019
answer
4
How was Idris' `rewrite` implemented?
Nov 27, 2017
answer
4
Fastest way to search a word in a word list?
Apr 7, 2018
Top Meta posts
1
0
3
What should I do if I miss-created a tag with a typo?
Top network posts
View all network posts
36
IntelliJ: changing color of an unused variable
33
How to implement this Java interface in Kotlin?
24
What is an algebraic data type?
24
How to apply a patch generated with git format-patch?
20
Are implicit arguments essential to (dependently-typed) proof assistants?

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.