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/
advanced?query=3136691