Principals in Programming Languages: Technical Results

Abstract

This is the companion technical report for ``Principals in Programming Languages'' [20]. 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 {\em principal}. The results are languages in which intuitive statements like ``the client must call $\mathtt{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.