First Advisor

Mark P. Jones

Term of Graduation

Winter 2022

Date of Publication


Document Type


Degree Name

Master of Science (M.S.) in Computer Science


Computer Science




Compilers (Computer programs), Mathematical optimization, Type theory



Physical Description

1 online resource (ix, 213 pages)


Compiler optimizations are critical to the efficiency of modern functional programs. At the same time, optimizations that unintentionally change the semantics of programs can systematically introduce errors into programs that pass through them. The question of how to best verify that optimizations and other program transformations preserve semantics is an important one, given the potential for error introduction. Dependent types allow us to prove that properties about our programs are correct, as well as to design data types and interpreters in such a way that they are correct-by-construction. In this thesis, we explore the use of dependent types and intrinsically-typed definitional interpreters in progressively larger subsets of Monadic Intermediate Language (MIL) to verify optimizations used in a compiler back end. In particular, we prove non-trivial program optimizations using the Agda proof assistant, and illustrate the benefits and challenges of this style of program verification.


In Copyright. URI: This Item is protected by copyright and/or related rights. You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s).

Persistent Identifier