AbstractsComputer Science

Typed Self-Optimization

by Matt Brown

Institution: UCLA
Department: Computer Science
Year: 2013
Keywords: Computer science; lambda calculus; optimization; self application; subtyping; type preservation; type systems
Record ID: 2005750
Full text PDF: http://www.escholarship.org/uc/item/1dt8m23m


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.