Proof Assistants Beta
Li-yao Xia's user avatar
Li-yao Xia's user avatar
Li-yao Xia's user avatar
Li-yao Xia
  • Member for 1 year, 9 months
  • Last seen more than a week ago
Profile Activity
Stats
1,517
reputation
5k
reached
25
answers
0
questions
Communities
View all
Badges
View all badges
This user doesn’t have any gold badges yet.
4
silver badges
11
bronze badges
Top tags
View all tags
48
Score
14
Posts
56
Posts %
26
Score
2
Posts
8
Posts %
18
Score
1
Posts
4
Posts %
11
Score
2
Posts
8
Posts %
11
Score
2
Posts
8
Posts %
8
Score
1
Posts
4
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
answer
18
Could proof assistants be used to prove that some piece of code is free of bugs?
Feb 8, 2022
answer
10
Expressivity of mutual/nested inductives vs. regular inductives
Mar 1, 2022
answer
8
How do Coq's bidirectionality hints (`&`) affect type checking?
May 24, 2022
answer
8
Proof Assistants for Vim Users
Feb 8, 2022
answer
8
Is internal parametricity useful in theorem proving?
Feb 9, 2022
answer
8
Seven Trees in One, or How to formalize the Semiring of Types?
Nov 3, 2022
answer
7
How do you import part of the standard library in Coq?
Feb 14, 2022
answer
5
Does ST$\lambda$C equal to simple type theory?
May 28, 2022
answer
5
Uses of first-class implicit function types
Dec 5, 2022
answer
5
Form of intros in Coq specifically for `forall` and explicitly for `->`
Feb 27, 2022
Top network posts
View all network posts
23
Polymorphism inside monads
22
Why do nested MaybeT's cause exponential allocation
20
Stack's package.yaml vs stack.yaml
18
How to Factorize Continuation Monad into Left & Right Adjoints?
18
What is the connection between laziness and purity?

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.