This is the companion technical report for "Principals in
Programming Languages: A Syntactic Proof Technique." See that document
for a more readable version of these results.
In this paper, we describe two variants of the simply typed
lambda-calculus extended with a notion of principal. The
results are languages in which intuitive statements like "the
client must call open to obtain a file handle" can be
phrased and proven formally.
The first language is a two-agent calculus with references and
recursive types, while the second language explores the possibility
of multiple agents with varying amounts of type information. We use
these calculi to give syntactic proofs of some type abstraction
results that traditionally require semantic arguments.