Theoretical Computer Science Stack Exchange

0

votes

0

answers

62

views

What is sequence unification?

lo.logic

asked Jun 16 at 2:20 Björn Lindqvist 229

3

votes

2

answers

168

views

How do continuations represent negations (under the Curry–Howard correspondence)?

lo.logic type-theory proof-theory continuations curry-howard

modified Jun 14 at 12:59 Dan Doel 381

3

votes

0

answers

39

views

Extending the sequential calculus (logic over words) to allow a hierarchy of languages like the arithmetical hierarchy

lo.logic fl.formal-languages first-order-logic

modified Jun 6 at 19:19 Emil Jeřábek 10.4k

3

votes

1

answer

112

views

Reductions in Descriptive Complexity

lo.logic reductions descriptive-complexity

modified May 31 at 8:26 Jan Johannsen 3,894

101

votes

7

answers

7k

views

Solid applications of category theory in TCS?

pl.programming-languages lo.logic ct.category-theory

answered May 8 at 9:06 michid 131

2

votes

0

answers

94

views

Notion of “quotient” or “inverse” for recognizable tree languages?

lo.logic fl.formal-languages automata-theory tree grammars

asked Apr 27 at 0:37 jmite 993

2

votes

2

answers

280

views

About the position of side conditions in an inference rule

lo.logic type-theory proof-theory

modified Apr 11 at 10:42 Andrej Bauer 22.4k

6

votes

2

answers

590

views

What logic correponds via Curry-Howard to a Monad?

lo.logic functional-programming ct.category-theory monad comonad

answered Apr 10 at 15:08 Henry Story 183

3

votes

2

answers

143

views

Compactness of domino tilings

co.combinatorics lo.logic computability automata-theory

modified Apr 1 at 6:59 Emil Jeřábek 10.4k

9

votes

2

answers

291

views

What is the benefit of Krivine's notation?

lo.logic lambda-calculus

answered Mar 27 at 21:54 Aaron Stump 11

1

vote

1

answer

108

views

Dependent C-style types with subtyping rule

lo.logic type-systems dependent-type

answered Mar 1 at 0:21 xrq 683

11

votes

2

answers

896

views

What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

lo.logic type-theory formal-modeling automated-theorem-proving bioinformatics

modified Feb 26 at 9:47 Glorfindel 173

65

votes

7

answers

3k

views

Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

cc.complexity-theory lo.logic pl.programming-languages big-picture set-theory

modified Feb 20 at 3:43 Timothy Chow 5,618

9

votes

1

answer

246

views

What is the reference for the proof Gödel's first incompleteness theorem based on the undecidability of the halting problem?

cc.complexity-theory lo.logic halting-problem

answered Feb 15 at 3:13 Yonatan N 1,187

Stack Exchange Network

current community

your communities

more stack exchange communities

Explore Our Questions

What is sequence unification?

How do continuations represent negations (under the Curry–Howard correspondence)?

Extending the sequential calculus (logic over words) to allow a hierarchy of languages like the arithmetical hierarchy

Reductions in Descriptive Complexity

Solid applications of category theory in TCS?

Notion of “quotient” or “inverse” for recognizable tree languages?

About the position of side conditions in an inference rule

What logic correponds via Curry-Howard to a Monad?

Compactness of domino tilings

What is the benefit of Krivine's notation?

Dependent C-style types with subtyping rule

What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?

Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)

What is the reference for the proof Gödel's first incompleteness theorem based on the undecidability of the halting problem?

Hot Network Questions