Sponsor
Portland State University. Department of Computer Science
First Advisor
Andrew Tolmach
Date of Publication
Summer 9-10-2019
Document Type
Thesis
Degree Name
Master of Science (M.S.) in Computer Science
Department
Computer Science
Language
English
Subjects
Type theory, Programming languages (Electronic computers)
DOI
10.15760/etd.7145
Physical Description
1 online resource (vi, 160 pages)
Abstract
Dependently-typed languages are well-known for the ability to enforce program invariants through type signatures, and previous work establishes the effectiveness of this style of program verification in the implementation of type-safe interpreters for a wide class of languages with a variety of interesting scoping semantics, offering an account of dynamic semantics. This thesis covers the complementary topic of static semantics, in the form of a pattern for constructing verified typechecking procedures in a dependently-typed setting. Implementations are given for simply-typed lambda calculus and a small procedural language as well as a module system with unrestricted cyclic module dependency semantics that are traditionally hard to formalize, parameterized over the choice of base language. A library of finite graphs and decision procedures for path search queries is presented and used in the construction of the example language implementations to resolve variable references. The resulting development is suitable as a static analysis phase ("middle end") in a hypothetical end-to-end verified interpreter developed in a dependently-typed setting.
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/30507
Recommended Citation
Casamento, Katherine Imhoff, "Correct-by-Construction Typechecking with Scope Graphs" (2019). Dissertations and Theses. Paper 5272.
https://doi.org/10.15760/etd.7145
Code artifact described in thesis
Comments
The code artifact described in the thesis is included as a supplemental zip file below.