Programming Language Semantics in Foundational Type Theory

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.