The approximation modality in models of higher-order types.

摘要

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.