Reasoning About Staged Programs

Files in this item

Files Size Format View
jun-inoue-masters-thesis.pdf 874.7Kb application/pdf Thumbnail

Show full item record

Item Metadata

Title: Reasoning About Staged Programs
Author: Inoue, Jun
Advisor: Taha, Walid
Degree: Master of Science thesis
Abstract: This thesis establishes formal equational properties of multi-stage calculi and related proof techniques that support analyses of staged programs. A key promise of staging is to make programs efficient without destroying clarity, thereby reducing the likelihood of bugs. However, few publications rigorously verify that their staged programs indeed behave as intended. In fact, little is known about how staged programs can be verified, or what correctness issues staging introduces. To solve this problem, I show a reduction of the correctness of a staged program to that of an unstaged program. This reduction not only clarifies the effects of staging on program behavior but also eases verification, as unstaged programs are more susceptible to existing reasoning techniques. I also demonstrate that important single-stage reasoning techniques apply to staged programs. These techniques are useful for establishing side conditions for the reduction and for discovering or validating further reasoning principles.
Citation: Inoue, Jun. (2010) "Reasoning About Staged Programs." Masters Thesis, Rice University.
Date: 2010

This item appears in the following Collection(s)