Skip to main content
Ilk's user avatar
Ilk's user avatar
Ilk's user avatar
Ilk
  • Member for 5 years, 11 months
  • Last seen more than a week ago
  • Somewhere
8 votes
4 answers
552 views

Type theory and fixed points of datatypes

7 votes
1 answer
1k views

Strongly normalizing type theory beyond induction-recursion

6 votes
0 answers
125 views

Programmatic higher inductive/inductive-inductive types with equalities between equalities

5 votes
0 answers
166 views

Non-trivial existence proof in type theory

5 votes
1 answer
400 views

Questions about P vs NP and geometric complexity theory

5 votes
0 answers
195 views

Abstract stone duality and cohesive homotopy type theory

5 votes
1 answer
346 views

How do we use directed univalence in directed type theory?

4 votes
0 answers
102 views

Relative consistency of various Martin-Löf style type theories

4 votes
0 answers
247 views

Rules between UIP with function extensionality and univalence

3 votes
0 answers
135 views

Graph problems in P with unknown lower bounds

3 votes
1 answer
139 views

Does a non-constructive proof of bounds of a computable asymptotic complexity, with impossible fix, exist?

3 votes
1 answer
173 views

Exposition of categorical models of type theory from type-theoretic perspective

2 votes
0 answers
84 views

Status of QNC vs. PSPACE

2 votes
1 answer
416 views

Extensional type theory and function extensionality

2 votes
1 answer
364 views

Non-termination, strict positivity and free monads

2 votes
0 answers
75 views

Categorical consequences in practical algorithms outside type theory

1 vote
1 answer
201 views

Defining normalization with respect to judgmental equality instead of reduction

1 vote
0 answers
86 views

What complexity class is characterized by having PSPACE verifiers?

1 vote
0 answers
65 views

Primitive recursion relative to a logical system

1 vote
1 answer
202 views

Extended Church's thesis and internal parametricity

0 votes
0 answers
49 views

Incompleteness and term extraction

0 votes
1 answer
328 views

Automatic theorem prover for first-order logic versus model checker