The Design and Implementation of a Safe, Lightweight Haskell Compiler

Abstract. Typed programming languages offer safety guarantees that help programmers write correct code, but typical language implemen-tations offer no proof that source-level guarantees extend to executable code. Moreover, typical implementations link programs with unsafe run-time system (RTS) code. I present a compiler for the functional language Haskell that preserves some of the properties of Haskell’s type system. The soundness proof for the combination of the compiler and a verified RTS requires a proof that the compiler emits code that cooperates cor-rectly with the RTS. In particular, the latter proof must address the boundary between the user program and the garbage collector. In this paper, I introduce a minimalist intermediate language type system that ensures that well-typed programs cannot make the garbage collector go wrong. I also discuss compilation strategies that allow simplifying the RTS. The work I present in this paper yields a simple and safe compila-tion system.