User Neel Krishnaswami

30 votes

4 answers

1k views

Are there "small" machines which can efficiently match regular expressions?

asked Sep 10, 2010 at 8:23

28 votes

6 answers

3k views

How should I think about proof nets?

lo.logic soft-question pl.programming-languages linear-logic

asked Jan 21, 2013 at 10:03

26 votes

1 answer

562 views

Interesting algorithms in the formalization of the Feit-Thompson theorem?

lo.logic proof-assistants

asked Sep 25, 2012 at 6:25

25 votes

2 answers

1k views

What is the folk model of linear logic?

pl.programming-languages ct.category-theory imperative-programming denotational-semantics linear-logic

asked Nov 8, 2010 at 14:26

24 votes

1 answer

583 views

Unification and Gaussian Elimination

reference-request lo.logic

asked Aug 16, 2012 at 5:37

19 votes

3 answers

3k views

Generalizations of Brzozowski's method of derivatives of regular expressions to grammars?

reference-request fl.formal-languages parsing

asked Nov 23, 2010 at 11:01

16 votes

1 answer

423 views

Parametricity and projective eliminations for dependent records

reference-request pl.programming-languages dependent-type parametricity

asked Jul 16, 2012 at 7:17

15 votes

2 answers

442 views

Proof theory of biproducts?

reference-request lo.logic pl.programming-languages type-theory ct.category-theory

asked Sep 9, 2011 at 9:18

15 votes

2 answers

449 views

Has anyone used Pottier and Gauthier's polymorphic defunctionalization in a modular compiler?

pl.programming-languages compilers

asked May 4, 2011 at 9:55

15 votes

1 answer

629 views

Fixed point theorems for constructive metric spaces?

reference-request lo.logic pl.programming-languages denotational-semantics metric-spaces

asked Apr 7, 2011 at 7:54

15 votes

2 answers

414 views

Uses of quasi-PERs/difunctional relations/zig-zag relations?

reference-request pl.programming-languages denotational-semantics logical-relations

asked Jul 3, 2012 at 14:11

15 votes

1 answer

485 views

Is MALL + unrestricted recursive types Turing-complete?

lo.logic pl.programming-languages linear-logic

asked Jan 8, 2013 at 8:22

14 votes

2 answers

296 views

Cut-elimination for calculus with nats or other inductive datatype?

lo.logic pl.programming-languages sequent-calculus

asked Dec 22, 2010 at 15:18

13 votes

0 answers

250 views

Generalizing limit-colimit coincidence to Scott-continuous adjunctions: any uses?

pl.programming-languages semantics denotational-semantics domain-theory

asked Oct 28, 2010 at 17:07

13 votes

1 answer

323 views

Relationship between shift-reduce parsing and delimited continuations?

pl.programming-languages parsing

asked Mar 28, 2012 at 5:15

12 votes

1 answer

376 views

When do coherence spaces have pullbacks and pushouts?

pl.programming-languages ct.category-theory domain-theory linear-logic

asked Jan 18, 2011 at 18:01

12 votes

1 answer

302 views

Reference for the fact that (0=1) implies false requires a universe in MLTT

reference-request lo.logic pl.programming-languages type-theory dependent-type

asked Jan 22, 2015 at 12:02

12 votes

0 answers

231 views

Categorical semantics for S5 modal logic?

reference-request lo.logic ct.category-theory proof-theory

asked Feb 18, 2017 at 13:29

11 votes

1 answer

339 views

Is Escardó's metric semantic for PCF+timeouts fully abstract ?

pl.programming-languages denotational-semantics metric-spaces

asked Mar 5, 2011 at 14:59

11 votes

2 answers

345 views

References to programming languages based on conditional logics

reference-request lo.logic pl.programming-languages type-theory proof-theory

asked Apr 12, 2011 at 9:08

10 votes

1 answer

308 views

Unification-based elimination rule for equality

reference-request lo.logic pl.programming-languages proof-theory sequent-calculus

asked May 4, 2012 at 11:02

10 votes

1 answer

190 views

Reference for the undefinability of modulus of continuity functional in PCF?

pl.programming-languages lambda-calculus denotational-semantics computing-over-reals

asked Jul 22, 2011 at 7:57

10 votes

0 answers

157 views

Do Banach spaces and linear contraction maps form a model of ILL with an exponential?

lo.logic linear-algebra ct.category-theory topology linear-logic

asked Sep 19, 2018 at 13:24

8 votes

1 answer

140 views

Hypersequents: proof term assigments or translations to hybrid logic

lo.logic pl.programming-languages proof-theory

asked Jul 11, 2014 at 15:22

8 votes

2 answers

269 views

Resumption-based IO systems?

reference-request pl.programming-languages functional-programming

asked Nov 26, 2012 at 14:55

8 votes

1 answer

235 views

Circuit complexity and statistical tests

circuit-complexity st.statistics

asked Sep 20, 2010 at 16:04

7 votes

0 answers

153 views

Does the cohomological approach to Boolean complexity nicely model any BDD heuristics?

ds.data-structures binary-decision-diagrams heuristics algebraic-topology

asked Apr 13, 2011 at 16:45

6 votes

1 answer

213 views

Has anyone studied "polynomially compact" metric spaces?

pl.programming-languages denotational-semantics metric-spaces

asked Jun 6, 2011 at 14:27

6 votes

0 answers

182 views

Relationship between Pataraia's theorem and inductive-recursive definitions?

lo.logic pl.programming-languages type-theory dependent-type fixed-points

asked Jun 27, 2017 at 16:00

6 votes

1 answer

249 views

Algebraic account of Gaussian elimination?

lo.logic linear-algebra matrices ct.category-theory linear-logic

asked Nov 3, 2017 at 14:16

Stack Exchange Network

current community

your communities

more stack exchange communities

35 Questions

Are there "small" machines which can efficiently match regular expressions?

How should I think about proof nets?

Interesting algorithms in the formalization of the Feit-Thompson theorem?

What is the folk model of linear logic?

Unification and Gaussian Elimination

Generalizations of Brzozowski's method of derivatives of regular expressions to grammars?

Parametricity and projective eliminations for dependent records

Proof theory of biproducts?

Has anyone used Pottier and Gauthier's polymorphic defunctionalization in a modular compiler?

Fixed point theorems for constructive metric spaces?

Uses of quasi-PERs/difunctional relations/zig-zag relations?

Is MALL + unrestricted recursive types Turing-complete?

Cut-elimination for calculus with nats or other inductive datatype?

Generalizing limit-colimit coincidence to Scott-continuous adjunctions: any uses?

Relationship between shift-reduce parsing and delimited continuations?

When do coherence spaces have pullbacks and pushouts?

Reference for the fact that (0=1) implies false requires a universe in MLTT

Categorical semantics for S5 modal logic?

Is Escardó's metric semantic for PCF+timeouts fully abstract ?

References to programming languages based on conditional logics

Unification-based elimination rule for equality

Reference for the undefinability of modulus of continuity functional in PCF?

Do Banach spaces and linear contraction maps form a model of ILL with an exponential?

Hypersequents: proof term assigments or translations to hybrid logic

Resumption-based IO systems?

Circuit complexity and statistical tests

Does the cohomological approach to Boolean complexity nicely model any BDD heuristics?

Has anyone studied "polynomially compact" metric spaces?

Relationship between Pataraia's theorem and inductive-recursive definitions?

Algebraic account of Gaussian elimination?