The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Intensional Analysis of Higher-Kinded Recursive Types

Last modified: Fri Oct 25 23:19:57 2002 GMT.

Authors

Gregory D. Collins
Zhong Shao

Abstract

Recursive types are ubiquitous in modern programming languages, as they occur when typing constructs such as datatype definitions. Any type-theoretic framework must effectively deal with recursive types if it purports to be applicable to real languages such as ML and Haskell. Intensional Type Analysis and Certified Binaries are two such type-theoretic frameworks. Previous work in these areas, however, has not adequately supported recursive types. In this paper we present a new formulation of recursive types which subsumes the traditional one. We show that intensional analysis over these types (including higher-kinded recursive types) can be supported via inductive elimination. Our solution is simple, general, and extensible; the typing rules for higher-kinded recursive types are concise and very easy to understand.

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