Language support for program generation: Reasoning, implementation, and applications

This dissertation develops programming languages and associated techniques for sound and efficient implementations of algorithms for program generation.; First, we develop a framework for practical two-level languages. In this framework, we demonstrate that two-level languages are not only a good tool for describing program-generation algorithms, but a good tool for reasoning about them and implementing them as well. We pinpoint several general properties of two-level languages that capture common proof obligations of program-generation algorithms: (1) To prove that the generated program that it behaves as desired, we use an erasure property to reduce the two-level proof obligation to a simpler one-level obligation. (2) To prove that the generated program satisfies certain syntactic constraints, we use a type-preservation property for a refined type system that enforces these constraints.; In addition, to justify concrete implementations, we use a native embedding of a two-level language into a one-level language.; We present two-level languages with these properties both for a call-by-name object language and for a call-by-value object language with computational effects, and demonstrate them through two classes of non-trivial applications: one-pass transformations into continuation-passing style and type-directed partial evaluation for call-by-name and for call-by-value.; Next, to facilitate implementations, we develop several general approaches to programming with type-indexed families of values within the popular Hindley-Milner type system. Type-indexed families provide a form of type dependency, which is employed by many algorithms that generate typed programs, but is absent from mainstream languages. Our approaches are based on type encodings, so that they are type safe. We demonstrate and compare them through a host of examples, including type-directed partial evaluation and printf-style formatting.; Finally, upon the two-level framework and type-encoding techniques, we recast a joint work with Bernd Grobauer, where we formally derived a suitable self application for type-directed partial evaluation, and achieved automatic compiler generation.