The Approximation Modality in Models of Higher-Order Types (thesis)
Report ID: TR-872-10Author: Richards, Christina
Date: 2010-04-00
Pages: 93
Download Formats: |PDF|
Abstract:
In this thesis we advance the state of the art in intensional type systems for low-level code. The need for powerful, carefully designed type-systems for low-level code is well-documented. We argue for an intensional, or semantic, such system, one which is distinguished by the use of a modality of type approximation to solve the problems of self-reference that arise in the models of recursive types, impredicative type quantification, and unrestricted mutable references.