Sciweavers

Share
ICFP
1999
ACM

Principals in Programming Languages: A Syntactic Proof Technique

8 years 10 months ago
Principals in Programming Languages: A Syntactic Proof Technique
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 λcalculus and show how we can track the code corresponding to each principal throughout evaluation. This multiagent yields syntactic proofs of some type abstraction properties that traditionally require semantic arguments.
Steve Zdancewic, Dan Grossman, J. Gregory Morriset
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 1999
Where ICFP
Authors Steve Zdancewic, Dan Grossman, J. Gregory Morrisett
Comments (0)
books