TACL Seminar Spring '04

From CSWiki
Revision as of 04:32, 27 August 2006 by Ddantas (talk | contribs) (Spring '04 Schedule)

Jump to: navigation, search

TACL Seminar

Spring '04 Schedule

Date Speaker Title Links
Feb 26 Aaron Stump (Wash U St. Louis) Static Validation of a Type-Preserving Compiler Abstract
Apr 16 Karl Crary (CMU) Grid Computing and Foundational Certified Code Abstract


Aaron Stump

Static Validation of a Type-Preserving Compiler

In their paper 'From System F to Typed Assembly Language', Morrisett, Walker, Crary, and Glew give a formal definition of a multi-stage compiler from a polymorphic functional programming language down to a (typed) assembly language. Each compiler stage is shown to be type-preserving: well-typed input programs are translated to well-typed output programs. This result is established for the mathematical description of the compiler stages, not an actual implementation of the compiler.

This talk describes work in progress to validate statically the following property of an actual implementation of the compiler: in the absence of certain run-time errors, any output program produced by a compiler stage for a typable input program is guaranteed to type check. This is achieved by writing the compiler in a proposed new language called Rogue-Sigma-Pi (RSP), which extends the Edinburgh Logical Framework (LF) with constructs for imperative programming with explicit recursion. A compiler stage is then written as a translation from proofs of typing judgments in the source language to proofs of typing judgments in the target language. RSP's type system can validate that proofs are manipulated in a sound way.

TACL Seminar