First Advisor

Andrew Tolmach

Date of Publication

Summer 9-10-2019

Document Type


Degree Name

Master of Science (M.S.) in Computer Science


Computer Science




Type theory, Programming languages (Electronic computers)



Physical Description

1 online resource (vi, 160 pages)


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.


In Copyright. URI: 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).


The code artifact described in the thesis is included as a supplemental zip file below.

Persistent Identifier

680917_supp_791342_59B77A92-CF6D-11E9-90F2-B93859571AF4 (1).zip (180 kB)
Code artifact described in thesis