Labbekak
  • Member for 3 years, 11 months
  • Last seen more than a week ago
  • Netherlands
0 answers
1 votes
24 views
Minimal cubical type theory to do coercion
0 answers
1 votes
26 views
Does Quantitative Type Theory make the Prop universe obsolete?
0 answers
0 votes
50 views
Is Observational Equality better than intensional equality?
0 answers
1 votes
28 views
Is there a most general fixpoint?
1 answers
10 votes
2k views
4 bookmarks
Why does Coq include let-expressions in its core language
0 answers
3 votes
76 views
Calculus of constructions, type-in-type and recursion
0 answers
3 votes
207 views
Type inference for System F-omega
1 answers
5 votes
80 views
2 bookmarks
What untyped term inhabits induction on natural numbers in CoC?
1 answers
2 votes
106 views
Optimization of Church-encoded booleans in System F
0 answers
1 votes
84 views
Call-by-push-value vs Fine-grain Call-by-value
1 answers
2 votes
56 views
Restrictions needed on ADT for totality
1 answers
5 votes
221 views
Abstractions in call-by-push-value
2 answers
4 votes
99 views
Composition of handler types in algebraic effects and handlers