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.
(dvi, pdf, ps)