Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Programming Language Semantics in Foundational Type Theory
Authors: Crary, Karl
Keywords: computer science
technical report
Issue Date: Mar-1998
Publisher: Cornell University
Abstract: There are compelling benefits to using foundational type theory as a framework for programming language semantics. I give a semantics of an expressive programming calculus in the foundational type theory of Nuprl. Previous type-theoretic semantics have used less expressive type theories, or have sacrificed important programming constructs such as recursion and modules. The primary mechanisms of this semantics for the core calculus are partial types, for typing recursion, set types, for encoding power and singleton kinds, which are used for subtyping and module programming, and very dependent function types, for encoding signatures. I then extend the semantics to modules using phase-splitting.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
98-1666.pdf364.88 kBAdobe PDFView/Open
98-1666.ps698.98 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us