First Advisor

Mark P. Jones

Term of Graduation

Winter 2022

Date of Publication

3-10-2022

Document Type

Thesis

Degree Name

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

Department

Computer Science

Language

English

Subjects

Compilers (Computer programs), Mathematical optimization, Type theory

DOI

10.15760/etd.7794

Physical Description

1 online resource (ix, 213 pages)

Abstract

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.

Rights

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).

Persistent Identifier

https://archives.pdx.edu/ds/psu/37367

Download

Share

COinS