Download Full Text

Citable link to this page

. . . . . .

Title:	Principals in Programming Languages: A Syntactic Proof Technique
Author:	Morrisett, John Gregory; Grossman, Dan; Zdancewic, Steve Note: Order does not necessarily reflect citation order of authors.
Citation:	Zdancewic, Steve, Dan Grossman, and Greg Morrisett. Principals in programming languages: A syntactic proof technique. In ICFP '99: Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP '99), Paris, France, September 27-29, 1999, ed. ICFP 1999, 197-207. ACM SIGPLAN Notices 34, no. 9. New York, N.Y.: Association for Computing Machinery.
Full Text & Related Files:	Morrisett_LanguagesSyntacticProof.pdf (202.3Kb; PDF)
Abstract:	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 calculus yields syntactic proofs of some type abstraction properties that traditionally require semantic arguments.
Published Version:	http://doi.acm.org/10.1145/317636.317799
Terms of Use:	This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAA
Citable link to this page:	http://nrs.harvard.edu/urn-3:HUL.InstRepos:2920217

Show full Dublin Core record

This item appears in the following Collection(s)

• FAS Scholarly Articles [5171]
  Peer reviewed scholarly articles from the Faculty of Arts and Sciences of Harvard University

Contact administrator regarding this item (to report mistakes or request changes)