Skip to main content
Łukasz Lew's user avatar
Łukasz Lew's user avatar
Łukasz Lew's user avatar
Łukasz Lew
  • Member for 6 years, 9 months
  • Last seen more than 2 years ago
  • Warsaw, Poland
10 votes
1 answer
361 views

Parametricity of Linear Logic

7 votes
1 answer
281 views

Does this variant of Multiplicative Linear Logic with mix rule enjoy cut elimination?

7 votes
2 answers
437 views

Is case analysis on normal forms of lambda terms sufficient to prove parametricity results?

6 votes
0 answers
253 views

Postulating self types in a proof assistant

6 votes
1 answer
801 views

Is Church-pentation implementable in Agda?

5 votes
1 answer
268 views

What's the difference between proving weak normalization and implementing evaluator?

5 votes
1 answer
481 views

Complexity of type-checking in relation to complexity of normalization

4 votes
1 answer
98 views

Why REFL rule is primitive in HOL Light?

4 votes
2 answers
165 views

What is the relation of HOL Light type theory and some of the intuitionistic type theories?

4 votes
1 answer
187 views

What is the relation of parametricity and function extensionality?

4 votes
1 answer
101 views

Is the set of Multiplicative Proof Nets a proper subset of set of well formed single-agent Interaction Nets?

3 votes
1 answer
230 views

Is there a 'very fast growing' hierarchy that would capture System F?

3 votes
0 answers
122 views

What's the example of natural transformation in 'Type" that is not a parametric function?

2 votes
1 answer
542 views

Is there a formalization of normalization of impredicative system F?

1 vote
0 answers
339 views

Is it possible to type Ackermann function with (stratified variant of) System F?

1 vote
1 answer
158 views

What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus?