SCS Undergraduate Thesis Topics

Michael Arntzenius Karl Crary A Type Theory of Linking

The processes of linking and loading, while fundamental to the way code is actually executed on modern computers, have hitherto evaded type-theoretic explanation. This prevents us from producing a typesafe linker and loader, which would satisfactorily close the gap between high-level typesafe programming languages and low-level typed assembly languages and proof-carrying code. We develop such a type theory, by way of defining the syntax and semantics of a lambda-calculus with explicit support for libraries. As a proof of concept, we implement a compiler from this calculus to a simple abstract machine language and associated object-file format, and an interpreter for this machine.

Close this window