Explore Our Questions

more tags

Active Hot Week Month

-2

votes

0

answers

23

views

Multiobjective Mixed Integer Linear Programming

cc.complexity-theory lo.logic linear-programming integer-programming polytope

modified 2 hours ago VS. 35

2

votes

2

answers

267

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 22k

6

votes

2

answers

515

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

134

views

Compactness of domino tilings

co.combinatorics lo.logic computability automata-theory

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

9

votes

2

answers

286

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

103

views

Dependent C-style types with subtyping rule

lo.logic type-systems dependent-type

answered Mar 1 at 0:21 xuq01 633

11

votes

2

answers

888

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 171

64

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,623

9

votes

1

answer

241

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,142

6

votes

2

answers

218

views

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

lo.logic type-theory normalization parametricity

answered Feb 12 at 19:21 gadmm 51

9

votes

1

answer

162

views

P and Descriptive Complexity

lo.logic polynomial-time descriptive-complexity

modified Feb 12 at 7:28 Hermann Gruber 3,930

14

votes

3

answers

2k

views

Symbolic Execution is a case of Abstract Interpretation?

reference-request lo.logic program-analysis

answered Jan 29 at 22:38 Patrick Cousot 21

6

votes

3

answers

280

views

When a type is a value?

lo.logic type-theory lambda-calculus functional-programming dependent-type

modified Jan 19 at 23:53 cody 11.4k

3

votes

0

answers

114

views

Busy Beaver Equivalent for the Untyped Lambda Calculus

lo.logic pl.programming-languages lambda-calculus

asked Jan 1 at 13:07 isaacg 333

Browse More Questions

Theoretical Computer Science Stack Exchange works best with JavaScript enabled