The ExSML project is a fork of Moscow ML which aims to replace the current MosML runtime with one based on LLVM. In Moscow ML the following things happen when you compile a file of SML source code: First the file is lexed and parsed into an abstract syntax tree. Then elaboration happens. In the elaboration phase we resolve, through type inference, the types of all expressions. We also resolve overloading such that all types are explicit from then on. Second the program is compiler by the frontend compiler into an Intermediate Representation (IR) called Lambda. This is an extended lambda calculus which is far simpler then core ML. At this step we also compile pattern matches into simple decision DAGs via a pattern match compiler by Peter Sestoft. The backend compiler then transforms lambda into bytecode which the mosml runtime reads and executes. We want to cut at the IR and produce LLVM code instead. However, there is a slight problem: LLVM is essentially a typed assembler whereas Lambda is untyped lambda calculus. To get around this, we have decided to use a typed variant of Lambda. This means we need a type system and we want the type system to be safe. Enter Twelf. The plan is to formalize the safety properties of the type system in Twelf. We are a far way from the goal at the moment as our Twelf-representation lacks many important things: reference operations, exceptions, reference state, recursive types, sum types, product types and polymorphism. But we hope to be able to add these to the representation with a little work. Knowing our language is type safe will give us some obvious advantages later on when we begin doing code transformations.