The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Intensional Analysis of Quantified Types

Last modified: Sun Aug 18 17:58:44 2002 GMT.

Authors

Bratin Saha
Valery Trifonov
Zhong Shao

Abstract

Compilers for polymorphic languages can use run-time type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data structures. Intensional type analysis is a type-theoretic framework for expressing and certifying such type-analyzing computations. Unfortunately, existing approaches to intensional analysis do not work well on quantified types such as existential or polymorphic types. This makes it impossible to code (in a type-safe language) applications such as garbage collection, persistency, or marshalling which must be able to examine the type of any run-time value.

We present a typed intermediate language that supports the analysis of quantified types. In particular, we provide both type-level and term-level constructs for analyzing quantified types. Our system supports structural induction on quantified types yet type checking remains decidable. We also show that our system is compatible with a type-erasure semantics.

Published

To appear in ACM Transactions on Programming Languages and Systems (TOPLAS), 51 pages, 2002.

Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon