|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/7363
| Title: | Formalizing Reference Types in NuPRL, PhD Thesis |
| Authors: | Naumov, Pavel |
| Keywords: | computer science
technical report |
| Issue Date: | Sep-1998 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR98-1709 |
| Abstract: | This dissertation defines a Type Theory based semantics for Java-like reference type constructors. The primary focus is made on finding an adequate axiomatization of reference types in Type Theory. An extension of Type Theory, called {\em Reference Type Theory}, is introduced. It adds to the Type Theory language a reference type constructor and operations on reference type elements as primitive notions. The dissertation provides informal graph-based semantics for the Reference Type Theory, describes inference rules for this theory, and proves their consistency. Reference Type Theory is formalized in the Nuprl Proof Development System. This formalization is used to define a formal semantics for a fragment of the Java programming language and to verify several simple Java programs. |
| URI: | http://hdl.handle.net/1813/7363 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
