¶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.

[Kutsia2002a]