Semantic specifications of programming languages can be used to assist or automate compiler generation. Semantics-driven compiler generation has already been studied for specification techniques such as denotational semantics, natural semantics, structural operational semantics and action semantics. Compilers generated from such specifications bring some of the performance benefits of traditional compilers to prototype specifications of programming languages while reducing or eliminating the logistical overhead of implementing a separate piece of software and proving its correctness.

This dissertation describes techniques that can be used to synthesize a compiler and virtual machine from a Substructural Operational Semantics (SSOS). Whereas prior work relied on techniques such as partial evaluation and staged computation to derive compilers from interpreters, we use linear logical approximations for synthesis. Our methodology is illustrated using language features from C0, a safe subset of C used to teach imperative programming at Carnegie Mellon University.

91 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]