Programs are often structured around the idea that different pieces of
code comprise distinct principals, each with a
view of its environment. Typical examples
include the modules of a large program, a host and its clients, or a
collection of interactive agents.
In this paper, we formalize this notion of principal in the
programming language itself. The result is a language in which
intuitive statements such as, "the client must call open
to obtain a file handle," can be phrased and proven formally.
We add principals to variants of the simply-typed
lambda-calculus and show how we can track the code corresponding
to each principal throughout evaluation. This
multiagent calculus yields syntactic proofs of some type abstraction
properties that traditionally require semantic arguments.