Skip to main content
eScholarship
Open Access Publications from the University of California

UCLA

UCLA Electronic Theses and Dissertations bannerUCLA

Typed Self-Optimization

Abstract

Researchers have studied how to type check self-applicable programs. For example, papers by Rendel, Ostermann, and Hofer, and by Jay and Palsberg have shown how to design two kinds of polymorphically typed self-interpreters. In this paper we present the first polymorphically typed self-optimizer. In contrast to a self-interpreter that often can implement each construct by itself, a self-optimizer may replace a subterm with a rather different subterm, which complicates type checking.

Our language has combinators, a variant of Mitchell's subtyping, proof terms that help match types, and a novel approach to type check self-application. Via syntactic sugar, we define a surface syntax with decidable type inference. Our implementation has type checked and run our examples.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View