A type-based escape analysis for functional languages

Research output: Contribution to journalArticle

8 Scopus citations

Abstract

An important issue faced by implementors of higher-order functional programming languages is the allocation and deallocation of storage for variables. The possibility of variables escaping their scope during runtime makes traditional stack allocation inadequate. We consider the problem of detecting when variables in such languages do not escape their scope, and thus can have their bindings allocated in an efficient manner. We use an annotated type system to infer information about the use of variables in a higher-order, strict functional language and combine this system with a translation to an annotated language which explicitly indicates which variables do not escape. The type system uses a notion of annotated types which extends the traditional simple type system with information about the extent of variables. To illustrate the use of this information we define an operational semantics for the annotated language which supports both stack and environment allocation of variable bindings. Only the stack allocated bindings need follow the protocol for stacks: their extent may not exceed their scope. Environment allocated bindings can have any extent, and their allocation has no impact on the stack allocated ones. We prove the analysis and translation correct with respect to this operational semantics by adapting a traditional type consistency proof to our setting. We have encoded the proof into the Elf programming language and typechecked it, providing a partially machine-checked proof.

Original languageEnglish (US)
Pages (from-to)239-273
Number of pages35
JournalJournal of Functional Programming
Volume8
Issue number3
DOIs
StatePublished - Jan 1 1998

All Science Journal Classification (ASJC) codes

  • Software

Fingerprint Dive into the research topics of 'A type-based escape analysis for functional languages'. Together they form a unique fingerprint.

  • Cite this