Theoretical Computer Science
Jesper's user avatar
Jesper's user avatar
Jesper's user avatar
Jesper
  • Member for 7 years, 9 months
  • Last seen more than a month ago
  • Netherlands
Profile Activity
Stats
356
reputation
1k
reached
6
answers
0
questions
Communities
View all
Badges
This user doesn’t have any gold badges yet.
1
silver badge
5
bronze badges
Top tags
View all tags
17
Score
4
Posts
67
Posts %
13
Score
5
Posts
83
Posts %
8
Score
1
Posts
17
Posts %
8
Score
1
Posts
17
Posts %
4
Score
2
Posts
33
Posts %
3
Score
1
Posts
17
Posts %
Top posts
All Questions Answers
Score Newest
answer
8
Small kernel (i.e. proof-verifier) for Agda?
Dec 4, 2019
answer
5
What's the effect of imposing the following restriction on inductive type families?
Jun 16, 2016
answer
3
What will go wrong if a recursive record type has a negative eta rule?
Mar 30, 2019
answer
3
Typing inference as a map on abstract syntax trees
Mar 14, 2021
answer
1
$\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$
Mar 22, 2021
answer
1
Is there a type theory system which includes an Any type
Jul 25, 2022
Top network posts
View all network posts
43
What is Axiom K?
15
What else can you do in the turn you ready an action?
13
Is it possible to get hold of free theorems as propositional equalities?
10
Why we cannot pattern match on Set/Type in Coq/Agda/Idris？
10
What subtyping rules does Agda support?

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.