Principals in Programming Languages: A Syntactic Proof Technique

Abstract

Programs are often structured around the idea that di#erent 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 #-calculus and show how we can track the code corresponding to each principal throughout evaluation. We use this multiagent calculus to give syntactic proofs of some type abstraction properties that traditionally require semantic arguments. 1 Introduction Programmers often have a notion of principal in mind when designing the structure of a program. Examples of such principals include modules of a large system, a host and its clients, and, ...