Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer's user avatar
Andrej Bauer
  • Member for 13 years, 6 months
  • Last seen this week
80 votes
Accepted

Techniques for Reversing the Order of Quantifiers

66 votes

To what extent is "advanced mathematics" needed/useful in A.I. research?

61 votes

What would it mean to disprove Church-Turing thesis?

49 votes
Accepted

A total language that only a Turing complete language can interpret

44 votes
Accepted

Is it possible to test if a computable number is rational or integer?

42 votes
Accepted

Why does Coq have Prop?

39 votes

Why colon to denote that a value belongs to a type?

37 votes

Problem teaching computability

35 votes

Realizability theory: difference in power between Lambda calculus and Turing Machines

34 votes
Accepted

What is the difference between arrows and exponential objects in a cartesian closed category?

33 votes
Accepted

Homotopy type theory and Gödel's incompleteness theorems

31 votes

Relationship between Turing Machine and Lambda calculus?

31 votes
Accepted

Why have computer scientists chosen recursor instead of iterator in primitive recursion?

26 votes

Solid applications of category theory in TCS?

26 votes
Accepted

How can we express "$P=PSPACE$" as a first-order formula?

25 votes

How can relational parametricity be motivated?

25 votes

Counterintuitive results for undergraduates

25 votes

What constitutes denotational semantics?

25 votes

Theoretical Computer Science vs other Sciences?

24 votes
Accepted

What's the point of $\eta$-conversion in lambda calculus?

24 votes
Accepted

Why it's impossible to declare an induction principle for Church numerals

22 votes

Why study type theory?

22 votes
Accepted

How exactly does lambda calculus capture the intuitive notion of computability?

22 votes
Accepted

Fixed point theorems for constructive metric spaces?

22 votes

What should a proof of correctness for a typechecker actually be proving?

21 votes
Accepted

Why do constructivists not seem to care too much about call/cc

21 votes
Accepted

What parts of homotopy type theory are not possible in Agda or Coq?

21 votes
Accepted

Difference between Types and Sorts

21 votes
Accepted

Proof relevance vs. proof irrelevance

20 votes
Accepted

Types which correspond to sets of cardinality of continuum

1
2 3 4 5
9