2022 Developer Survey is open! Take survey.
user avatar
user avatar
user avatar
Labbekak
  • Member for 4 years, 3 months
  • Last seen more than a month ago
  • Netherlands
10 votes
1 answer
2k views

Why does Coq include let-expressions in its core language

5 votes
1 answer
82 views

What untyped term inhabits induction on natural numbers in CoC?

5 votes
1 answer
241 views

Abstractions in call-by-push-value

4 votes
2 answers
102 views

Composition of handler types in algebraic effects and handlers

3 votes
0 answers
226 views

Type inference for System F-omega

3 votes
0 answers
81 views

Calculus of constructions, type-in-type and recursion

2 votes
1 answer
59 views

Restrictions needed on ADT for totality

2 votes
1 answer
112 views

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

2 votes
1 answer
114 views

Optimization of Church-encoded booleans in System F

1 vote
0 answers
32 views

Is there a most general fixpoint?

1 vote
0 answers
27 views

Does Quantitative Type Theory make the Prop universe obsolete?

1 vote
0 answers
28 views

Minimal cubical type theory to do coercion

0 votes
0 answers
63 views

Is Observational Equality better than intensional equality?