A collection of papers in sequence for reference in the development of this type theory. Linear-Dependent Type Theories Mcbride, Conor. I Got Plenty o' Nuttin' a. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: a calculus ofcontext-dependent computation