User Andrej Bauer

79 votes

Accepted

Techniques for Reversing the Order of Quantiﬁers

answered Jan 22, 2011 at 9:30

64 votes

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

answered Oct 19, 2012 at 13:27

61 votes

What would it mean to disprove Church-Turing thesis?

answered Sep 2, 2010 at 14:40

49 votes

Accepted

A total language that only a Turing complete language can interpret

answered Jun 24, 2014 at 8:19

42 votes

Accepted

Why does Coq have Prop?

answered Mar 31, 2014 at 5:07

42 votes

Accepted

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

answered Feb 19, 2013 at 7:22

39 votes

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

answered May 25, 2019 at 13:43

37 votes

Problem teaching computability

answered Feb 20, 2011 at 20:28

35 votes

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

answered Sep 9, 2010 at 21:46

34 votes

Accepted

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

answered Apr 17, 2013 at 9:46

33 votes

Accepted

Homotopy type theory and Gödel's incompleteness theorems

answered Apr 16, 2014 at 6:25

31 votes

Relationship between Turing Machine and Lambda calculus?

answered Aug 28, 2010 at 21:11

31 votes

Accepted

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

answered Jun 18, 2011 at 6:18

26 votes

Solid applications of category theory in TCS?

answered Sep 4, 2010 at 17:11

26 votes

Accepted

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

answered Feb 25, 2013 at 14:02

25 votes

How can relational parametricity be motivated?

answered Oct 27, 2013 at 21:10

25 votes

Counterintuitive results for undergraduates

answered May 26, 2015 at 17:58

25 votes

What constitutes denotational semantics?

answered Dec 6, 2010 at 14:53

25 votes

Theoretical Computer Science vs other Sciences?

answered Mar 13 at 20:24

24 votes

Accepted

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

answered Sep 19, 2011 at 0:00

24 votes

Accepted

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

answered Mar 25, 2015 at 22:19

22 votes

Accepted

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

answered Feb 12, 2015 at 7:07

22 votes

Accepted

Fixed point theorems for constructive metric spaces?

answered Apr 7, 2011 at 9:20

22 votes

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

answered Jun 12, 2017 at 9:00

21 votes

Accepted

Proof relevance vs. proof irrelevance

answered Dec 30, 2020 at 15:14

21 votes

Accepted

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

answered Apr 6, 2015 at 21:29

21 votes

Why study type theory?

answered Mar 12, 2015 at 7:47

21 votes

Accepted

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

answered Feb 22, 2014 at 15:21

20 votes

Accepted

Types which correspond to sets of cardinality of continuum

answered May 7, 2014 at 20:38

20 votes

Accepted

Difference between Types and Sorts

answered Jul 9, 2013 at 12:14

Stack Exchange Network

258 Answers

Techniques for Reversing the Order of Quantiﬁers

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

What would it mean to disprove Church-Turing thesis?

A total language that only a Turing complete language can interpret

Why does Coq have Prop?

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

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

Problem teaching computability

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

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

Homotopy type theory and Gödel's incompleteness theorems

Relationship between Turing Machine and Lambda calculus?

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

Solid applications of category theory in TCS?

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

How can relational parametricity be motivated?

Counterintuitive results for undergraduates

What constitutes denotational semantics?

Theoretical Computer Science vs other Sciences?

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

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

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

Fixed point theorems for constructive metric spaces?

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

Proof relevance vs. proof irrelevance

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

Why study type theory?

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

Types which correspond to sets of cardinality of continuum

Difference between Types and Sorts