First Advisor

Tim Sheard

Date of Publication

11-2008

Document Type

Dissertation

Degree Name

Doctor of Philosophy (Ph.D.) in Computer Science

Department

Computer Science

Language

English

Subjects

Type theory, Functional programming (Computer science), Computer software -- Development

DOI

10.15760/etd.2669

Physical Description

1 online resource (ix, 315 pages)

Abstract

Dependent type theory is a proven technology for verified functional programming in which programs and their correctness proofs may be developed using the same rules in a single formal system. In practice, large portions of programs developed in this way have no computational relevance to the ultimate result of the program and should therefore be removed prior to program execution. In previous work on identifying and removing irrelevant portions of programs, computational irrelevance is usually treated as an intrinsic property of program expressions. We find that such an approach forces programmers to maintain two copies of commonly used datatypes: a computationally relevant one and a computationally irrelevant one.

We instead develop an extrinsic notion of computational irrelevance and find that it yields several benefits including (1) avoidance of the above mentioned code duplication problem; (2) an identification of computational irrelevance with a highly general form of parametric polymorphism; and (3) an elective (i.e., user-directed) notion of proof irrelevance. We also develop a program analysis for identifying irrelevant expressions and show how previously studied types embodying computational irrelevance (including subset types and squash types) are expressible in the extension of type theory developed herein.

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

Comments

If you are the rightful copyright holder of this dissertation or thesis and wish to have it removed from the Open Access Collection, please submit a request to pdxscholar@pdx.edu and include clear identification of the work, preferably with URL

Persistent Identifier

http://archives.pdx.edu/ds/psu/16546

Download

Share

COinS