Portland State University. Department of Computer Science
Date of Award
Master of Science (M.S.) in Computer Science
1 online resource (vi, 160 pages)
Type theory, Programming languages (Electronic computers)
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.
Casamento, Katherine Imhoff, "Correct-by-Construction Typechecking with Scope Graphs" (2019). Dissertations and Theses. Paper 5272.