Skip to main content


Showing posts from December, 2014

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 types of bugs exi…

What do concurrent traces have to say about determinism?

Let's talk about execution traces of concurrent programs, and which ones we consider "the same."

In concurrent programming models, your program constructs allow you to specify computation as indexed by a particular independent execution unit ("thread", "channel", "actor" -- at this level of detail, we can use these terms interchangeably), and to specify how those units communicate or interact. This means you have one artifact, the static program, that gives rise to a set of traces, or possible executions -- records of which parts of the program were evaluated in what order.

We might say that if this set of program traces has only one element, then the program is sequential. But the accuracy of this statement depends on how exactly we represent a program trace! If we are forced to give a total ordering on all computation steps -- unifying a trace with an "interleaving of instructions" -- then yes, the only class of programs for whic…

Design a PL for Knitting at Disney Research Pittsburgh!

My friend Jim just told me about an exciting-sounding internship opportunity for Ph.D. students in programming languages! Check it out:

Disney Research Pittsburgh seeks a PhD student with experience in Programming Languages or Compilers for a summer internship. The student will be expected to apply programming language methods to the analysis and control of knitting machines, with potential topics including:  developing a semantics for machine knitting  formally describing a notion of machine knittability  inverse knitting  knit scheduling  knitting pattern optimization  knitting failure analysis and robustness estimation  translation from hand knitting to machine knitting As part of the internship, the student will write up their work for submission to an appropriate top-tier venue; applicants with prior publications in such venues will be strongly favored. Interested students should contact Jim McCann ( to arrange a further conversation. Please include or …