Skip to main content
Computer Science
Labbekak's user avatar
Labbekak's user avatar
Labbekak's user avatar
Labbekak
  • Member for 6 years, 10 months
  • Last seen more than a month ago
  • Netherlands
Profile Activity

13 Questions

Score Activity Newest Views
12 votes
2 answers
3k views

Why does Coq include let-expressions in its core language

5 votes
1 answer
106 views

What untyped term inhabits induction on natural numbers in CoC?

5 votes
1 answer
304 views

Abstractions in call-by-push-value

4 votes
2 answers
147 views

Composition of handler types in algebraic effects and handlers

3 votes
0 answers
579 views

Type inference for System F-omega

3 votes
0 answers
120 views

Calculus of constructions, type-in-type and recursion

2 votes
1 answer
76 views

Restrictions needed on ADT for totality

2 votes
1 answer
319 views

Call-by-push-value vs Fine-grain Call-by-value

2 votes
1 answer
156 views

Optimization of Church-encoded booleans in System F

2 votes
0 answers
164 views

Is Observational Equality better than intensional equality?

1 vote
0 answers
45 views

Does Quantitative Type Theory make the Prop universe obsolete?

1 vote
0 answers
44 views

Minimal cubical type theory to do coercion

1 vote
0 answers
36 views

Is there a most general fixpoint?