Kleffner's talk on stack language typing

Rob Kleffner gave a talk in March 2017 at a PRL group seminar at Northeastern, entitled “Type Inference in Stack-Based Programming Languages”. He has some really useful background notes and an annotated bibliography.

• He mentions that “Kutsia 2002” shows that “sequence unification is unitary” when the sequence variable is restricted to being in the left-most position. Need to track down precisely which paper this refers to, but it would provide a nice proof of the efficiency of our stack graph unification algorithm, which has the same static constraint on partial path pre- and postconditions.