Stateful Contracts for Affine Types

Jesse A. Tov and Riccardo Pucella

In Proc. 19th European Symposium on Programming (ESOP ’10), March 2010

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 components 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 behavioral contracts to mediate between code written in an affine language and code in a conventional 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.

Available:

• Extended version (with proofs):
  • color (PDF, 998 KiB)
  • black and white (PDF, 982 KiB)
• Shorter version (no proofs):
  • color (PDF, 331 KiB)
  • black and white (PDF, 330 KiB)
• Slides from talk (PDF, 580 KiB)
• Prototype implementation (Haskell source)
• PLT Redex Model (What is PLT Redex?)
• PLaneT package (Affine contracts for PLT Scheme)

Shorter version of ``Stateful Contracts for Affine Types'' paper © 2010 Springer-Verlag. Please do not redistribute.

---

Publications list | Home