What do you think?
Rate this book
Irrelevance, Polymorphism, and Erasure in Type Theory
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.
reply | flag
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.
reply | flag
329 pages, ebook
Published November 1, 2008
1 person want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 of 1 review
September 6, 2024
Perhaps dated now that we have Atkey/McBride's QTT, dependent dependency calculus, and other similar developments, but it's still a quite well-written thesis and worth going through if just for the motivation and intuition behind erasure.
Although, I didn't fully understand the ITPS system (Γ ⊢ x : A seems to be derivable even if x isn't in Γ, which doesn't make sense, although that's not a problem in practice since such derivations aren't in the image of ETPS under the erasure) and the realizability stuff, but I just don't know much about realizability in the first place.
Although, I didn't fully understand the ITPS system (Γ ⊢ x : A seems to be derivable even if x isn't in Γ, which doesn't make sense, although that's not a problem in practice since such derivations aren't in the image of ETPS under the erasure) and the realizability stuff, but I just don't know much about realizability in the first place.
Displaying 1 of 1 review