User Joey Eremondi

26 votes

6 answers

2k views

Advanced techniques for determining complexity lower bounds

asked Jul 22, 2013 at 17:23

21 votes

5 answers

843 views

What notable automaton models have polynomially-decidable containment?

asked Jun 16, 2014 at 17:37

16 votes

1 answer

536 views

Are there variants of visibly pushdown automata that allow pushing of words onto the stack?

asked Jul 18, 2013 at 17:42

12 votes

1 answer

386 views

Is there a book/survey-paper outlining language class hierarchies, closure properties, etc

asked May 28, 2013 at 20:05

12 votes

2 answers

456 views

State of the Art for the Monadic Class?

asked Nov 5, 2017 at 8:04

12 votes

1 answer

947 views

Proof techniques for showing that dependent type checking is decidable

asked Oct 11, 2018 at 4:59

12 votes

2 answers

728 views

Intuition Behind Strict Positivity?

asked Apr 2, 2019 at 0:27

11 votes

2 answers

438 views

Hereditary substitution with a universe hierarchy

asked Nov 22, 2018 at 23:02

8 votes

1 answer

513 views

PHOAS with extrinsic typing?

asked Nov 26, 2019 at 5:16

7 votes

1 answer

452 views

Avoiding Cycles with Unification and Subtyping

asked Mar 26, 2018 at 2:16

7 votes

1 answer

130 views

Quanitifier Free Presburger Arithmetic: Upper bound on solution size?

asked Jan 24, 2015 at 14:32

6 votes

2 answers

439 views

Preservation under Substitution with Telescopes

asked Oct 29, 2018 at 23:25

6 votes

2 answers

295 views

Typing of substitution in a bidirectional type system

asked Nov 1, 2018 at 18:56

6 votes

2 answers

187 views

Are deterministic context-free languages closed under outfix (or other erasing operations)

asked Jul 4, 2014 at 17:56

6 votes

0 answers

391 views

Reverse Skolemization?

asked Jul 7, 2019 at 18:14

6 votes

1 answer

169 views

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

asked Jul 24, 2019 at 16:45

6 votes

1 answer

232 views

Structural equality of Pi Types with heterogeneous equality?

asked Sep 30, 2019 at 17:33

6 votes

1 answer

317 views

Fixed set of type constructors to simulate all intensional inductive families?

asked Sep 30, 2019 at 19:12

5 votes

1 answer

176 views

What language $L \in NCM$ has $\overline{L} \not \in NCM$?

asked Jul 30, 2014 at 21:38

5 votes

1 answer

257 views

Can emptiness of reversal-bounded counter languages be decided in time polynomial to the number of counters?

asked Jul 4, 2013 at 21:56

4 votes

1 answer

278 views

What characterizations exist for the grammars that can express subsets of the context-free languages?

asked Jul 4, 2014 at 18:12

4 votes

0 answers

169 views

Hereditary Substitution with Inductives and Eliminators?

asked Jan 30, 2019 at 22:15

4 votes

0 answers

118 views

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

asked Feb 11, 2019 at 22:04

3 votes

1 answer

153 views

Notion of "quotient" or "inverse" for recognizable tree languages?

asked Apr 27, 2019 at 0:37

3 votes

0 answers

154 views

Set:Set or Negative Inductives in a Total Language?

asked Jan 22, 2020 at 19:36

2 votes

1 answer

83 views

Nominal Tree Languages i.e. with Binders and Infinite Symbols?

asked Oct 19, 2020 at 22:49

2 votes

0 answers

70 views

Regular Tree Languages are closed under quotient?

asked Apr 25, 2019 at 22:31

2 votes

1 answer

102 views

Are Reversal-bounded Multicounter Machines closed under reversal?

asked Jun 3, 2013 at 17:17

2 votes

1 answer

116 views

Is it decidable whether the langauge accepted by a reversal-bounded counter machine is deterministic?

asked Jul 3, 2013 at 16:30

1 vote

0 answers

482 views

Equality Constraints over Sets with Tree Automata

asked Oct 7, 2017 at 21:13

Stack Exchange Network

30 Questions

Advanced techniques for determining complexity lower bounds

What notable automaton models have polynomially-decidable containment?

Are there variants of visibly pushdown automata that allow pushing of words onto the stack?

Is there a book/survey-paper outlining language class hierarchies, closure properties, etc

State of the Art for the Monadic Class?

Proof techniques for showing that dependent type checking is decidable

Intuition Behind Strict Positivity?

Hereditary substitution with a universe hierarchy

PHOAS with extrinsic typing?

Avoiding Cycles with Unification and Subtyping

Quanitifier Free Presburger Arithmetic: Upper bound on solution size?

Preservation under Substitution with Telescopes

Typing of substitution in a bidirectional type system

Are deterministic context-free languages closed under outfix (or other erasing operations)

Reverse Skolemization?

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

Structural equality of Pi Types with heterogeneous equality?

Fixed set of type constructors to simulate all intensional inductive families?

What language $L \in NCM$ has $\overline{L} \not \in NCM$?

Can emptiness of reversal-bounded counter languages be decided in time polynomial to the number of counters?

What characterizations exist for the grammars that can express subsets of the context-free languages?

Hereditary Substitution with Inductives and Eliminators?

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Notion of "quotient" or "inverse" for recognizable tree languages?

Set:Set or Negative Inductives in a Total Language?

Nominal Tree Languages i.e. with Binders and Infinite Symbols?

Regular Tree Languages are closed under quotient?

Are Reversal-bounded Multicounter Machines closed under reversal?

Is it decidable whether the langauge accepted by a reversal-bounded counter machine is deterministic?

Equality Constraints over Sets with Tree Automata