Proof Assistants Beta
ice1000's user avatar
ice1000's user avatar
ice1000's user avatar
ice1000
  • Member for 1 year, 10 months
  • Last seen this week
Profile Activity
Stats
5,877
reputation
31k
reached
38
answers
51
questions
Communities
View all
About

I'm into univalent type systems. Worked on Agda and Arend, working on Aya.

Visit count (since 23 Feb 2023):

Badges
View all badges
This user doesn’t have any gold badges yet.
9
silver badges
59
bronze badges
Top tags
View all tags
63
Score
20
Posts
22
Posts %
49
Score
13
Posts
15
Posts %
22
Score
7
Posts
8
Posts %
15
Score
5
Posts
6
Posts %
14
Score
7
Posts
8
Posts %
13
Score
5
Posts
6
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
question
29
What is an algebraic data type?
Feb 27, 2022
question
20
Are implicit arguments essential to (dependently-typed) proof assistants?
Feb 8, 2022
question
18
What are the advantages of normalization by evaluation over traditional reduction-based normalization?
Feb 9, 2022
question
18
What's the difference between reflection and tactics?
Mar 19, 2022
question
17
Is internal parametricity useful in theorem proving?
Feb 9, 2022
question
16
How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Mar 27, 2022
question
15
What happened to Conor McBride's universe polymorphism proposal?
Feb 9, 2022
question
15
How to represent mathematical partial functions in a type-theory based proof assistant?
Feb 15, 2022
question
14
Is there any example of a dependent product that makes sense in a non-type-theory context?
Mar 19, 2022
answer
14
In Agda, why is universe polymorphism explicit?
Feb 10, 2022
Top Meta posts
2
0
4
How detailed should tags be?
3
Should I create tags for common components in proof assistant implementations?
Top network posts
View all network posts
41
IntelliJ: changing color of an unused variable
39
What are different ways of handling runtime errors?
36
How to implement this Java interface in Kotlin?
35
Why do some programming languages choose to have a dedicated keyword for elseif instead of using else + if like in C?
31
What are the drawbacks of using indentation for code blocks?

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.