Intensional analysis of quantified types

Autor:	Bratin Saha, Valery Trifonov, Zhong Shao
Rok vydání:	2003
Předmět:	Intermediate language Programming language Computer science computer.software_genre Data structure Decidability Marshalling TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Structural induction Compiler computer Garbage Software Garbage collection
Zdroj:	ACM Transactions on Programming Languages and Systems. 25:159-209
ISSN:	1558-4593 0164-0925
DOI:	10.1145/641888.641889
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::3afbaf3fe421cab22f598baa824069cf https://doi.org/10.1145/641888.641889 Zobrazit plný text záznamu