The Approximation Modality in Models of Higher-Order Types (thesis)

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.