i Contents Contents Contents

Affine type systems manage resources by preventing some values from being used more than once. This offers expressiveness and performance benefits, but difficulty arises in interacting with com-ponents written in a conventional language whose type system provides no way to maintain the affine type system’s aliasing invariants. We propose and implement a technique that uses be-havioral contracts to mediate between code written in an affine language and code in a conven-tional typed language. We formalize our approach via a typed calculus with both affine-typed and conventionally-typed modules. We show how to preserve the guarantees of both type systems despite both languages being able to call into each other and exchange higher-order values. This is the extended version of a paper that appeared in ESOP 2010