Accumulated Braindust
Conor McBride posted a really intriguing list of research problems on his mind at the end of this year, and I thought it was an amazing idea, so I'm copying it. I have little notes I've made to myself in paper notebooks and text files, but rarely do I go through and collect them all in one place. Computer-checking linear logic program invariants (and other, perhaps variant, properties) - what is an appropriate metalogic to reason about linear proof search? Generative invariants : what is their expressive range? Does it have something to do with (co)inductive datatypes or their dependent generalization? Can we extend them to describe general structures such as graphs (with no self-edges or multi-edges), perhaps by allowing quantification over, and introduction to, *sets* of terms rather than types? Ordered logic - are there more connectives? constrained replication and mobility, e.g. a propositional operator *A meaning A can be replicated "in place." What type