LEADER 00000nam  2200313   4500 
001    AAI3136691 
005    20051017073520.5 
008    051017s2004                        eng d 
020    0496838873 
035    (UnM)AAI3136691 
040    UnM|cUnM 
100 1  Ahmed, Amal Jamil 
245 10 Semantics of types for mutable state 
300    246 p 
500    Source: Dissertation Abstracts International, Volume: 65-
       06, Section: B, page: 2994 
502    Thesis (Ph.D.)--Princeton University, 2004 
520    Proof-carrying code (PCC) is a framework for mechanically 
       verifying the safety of machine language programs. A 
       program that is successfully verified by a PCC system is 
       guaranteed to be safe to execute, but this safety 
       guarantee is contingent upon the correctness of various 
       trusted components. For instance, in traditional PCC 
       systems the trusted computing base includes a large set of
       low-level typing rules. Foundational PCC systems seek to 
       minimize the size of the trusted computing base. In 
       particular, they eliminate the need to trust complex, low-
       level type systems by providing machine-checkable proofs 
       of type soundness for real machine languages 
520    In this thesis, I demonstrate the use of logical relations
       for proving the soundness of type systems for mutable 
       state. Specifically, I focus on type systems that ensure 
       the safe allocation, update, and reuse of memory. For each
       type in the language, I define logical relations that 
       explain the meaning of the type in terms of the 
       operational semantics of the language. Using this model of
       types, I prove each typing rule as a lemma 
520    The major contribution is a model of System F with general
       references---that is, mutable cells that can hold values 
       of any closed type including other references, functions, 
       recursive types, and impredicative quantified types. The 
       model is based on ideas from both possible worlds and the 
       indexed model of Appel and McAllester 
520    I show how the model of mutable references is encoded in 
       higher-order logic. I also show how to construct an 
       indexed possible-worlds model for a von Neumann machine. 
       The latter is used in the Princeton Foundational PCC 
       system to prove type safety for a full-fledged low-level 
       typed assembly language. Finally, I present a semantic 
       model for a region calculus that supports type-invariant 
       references as well as memory reuse 
590    School code: 0181 
590    DDC 
650  4 Computer Science 
690    0984 
710 20 Princeton University 
773 0  |tDissertation Abstracts International|g65-06B 
856 40 |uhttp://pqdd.sinica.edu.tw/twdaoapp/servlet/