Leaf's Thesis Proposal

[Stephen Weeks]

Matthew, in case you didn't see it, here is Leaf's proposal announcement.  It
looks to be related to the kinds of things we were talking about in terms of
making MLton's backend/codegen use typed ILs.

> ----------------------------------------------------------------------
> Dates:    28-Sep-2001
> Time:     2:00 pm
> Place:    NSH 3305
> Type:     Thesis Proposal
> Who:      Leaf Eames Petersen
> Topic:    Certifying compilation for Standard ML in a type analysis
> framework.
> 
>                         ABSTRACT
> 
> Certified code is native machine code that is annotated with an
> automatically checkable certificate attesting to the conformance of the
> program to a specified safety policy.  Certified code frameworks have
> been built based on first-order logic (PCC) and on types (TAL).
> Compilers generating certified code have been built for safe subsets of
> C and for Java(tm).
> 
> Type-preserving compilers such as the TILT/ML compiler implement
> compilation as transformations on typed internal languages.  Types are
> used by the compiler for internal verification, and for optimization
> purposes.  Type analysis can be used to implement optimizations such as
> non-uniform data representation and tag-free garbage collection.
> However, none of the existing type-preserving compilers for full-scale
> languages maintain type information all the way to the machine-code
> level, and hence are not yet able to generate certified code.
> 
> I propose to extend the TILT/ML compiler to generate certified code in
> the form of typed assembly language without compromising the existing
> optimizations of the compiler. The goal of this work is to show that a
> compiler can use types to generate certified binaries for a full modern
> language even in the presence of agressive type-analysis based
> optimization.
> 
> FurtherDetails:
> 
> Thesis Committee:
> Robert Harper (Chair)
> Karl Crary
> Peter Lee
> Greg Morrisett, Cornell University