Portland State University. Department of Computer Science
Mark P. Jones
Term of Graduation
Date of Publication
Master of Science (M.S.) in Computer Science
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: http://rightsstatements.org/vocab/InC/1.0/ 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).
Barrack, Dani, "Using Intrinsically-Typed Definitional Interpreters to Verify Compiler Optimizations in a Monadic Intermediate Language" (2022). Dissertations and Theses. Paper 5923.