Type Checking Program Generators Using the Record Calculus

Abstract

Program Generation (PG) is about writing programs that write programs. A program generator composes various pieces of code to construct a new program. An important challenge of PG that has been studied widely is how to ensure that a generator will produce type-safe code. We address the same problem by showing that record calculus can be used to obtain a type system for program generation. We first show that operational semantics of record calculus and program generation are equivalent, and that a record type system can be used to type-check program generators. We also show that this is true in the presence of expressions with side-effects. The record type system yields a type system that is equal to Kim, Yi and Calcagno's staged type system. We then make use of an already-existing record calculus feature, subtyping, to extend the program generation type system with subtyping constraints. As a result, we obtain a very expressive type system to statically guarantee that a generator will produce type-safe code. We state and prove the theorems based on an ML-like language with program generation constructs.

Short bio

Baris Aktemur received his B.S. degree from the Computer Engineering Department of Bilkent University, Ankara, Turkey in 2003. He then received his M.S. and Ph.D. degrees from the University of Illinois at Urbana-Champaign, USA, in 2005 and 2009, respectively, both in Computer Science. His research interests include theory and applications of runtime program generation, programming language design and analysis, type theory, and software engineering. Baris Aktemur will be with the Faculty of Engineering of Ozyegin University, Istanbul, Turkey, starting Fall 2009.

Resources

• talk slide