Advisor

Andrew Tolmach

Date of Award

9-10-2019

Document Type

Thesis

Degree Name

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

Department

Computer Science

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.

Description

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

Persistent Identifier

https://archives.pdx.edu/ds/psu/30507

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

Share

COinS