Files in this item



application/pdf3017092.pdf (7MB)Restricted to U of Illinois
(no description provided)PDF


Title:Modular Compilers and Their Correctness Proofs
Author(s):Harrison, William Lawrence
Doctoral Committee Chair(s):Kamin, Samuel N.
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Science
Abstract:This thesis explores the construction and correctness of modular compilers. Modular compilation is a compiler construction technique allowing the construction of compilers for high-level programming languages from reusable compiler building blocks. Modular compilers are defined in terms of denotational semantics based on monads, monad transformers, and a new model of staged computation called metacomputations. A novel form of denotational specification called observational program specification and related proof techniques are developed to assist in modular compiler verification. It will be demonstrated that the modular compilation framework provides both a level of modularity in compiler proofs as well as a useful organizing principle for such proofs.
Issue Date:2001
Description:283 p.
Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 2001.
Other Identifier(s):(MiAaPQ)AAI3017092
Date Available in IDEALS:2015-09-25
Date Deposited:2001

This item appears in the following Collection(s)

Item Statistics