An Agda scope checker implemented in Agda

Abstract

Agda [1] is a Haskell-style, purely functional, dependently typed programming language and theorem prover. Scope checking is the process of analyzing the Abstract Syntax Tree (AST) of a program and resolving all references to symbols by connecting them to the corresponding declarations of said symbols. The Agda scope checker – as well as the rest of the compiler – is written in Haskell, and does not include any proof about the reachability of declarations. In this thesis, we present a scope checker for the Agda language, written in Agda itself, and prove the correctness of its name resolution algorithm with reference to the reachability properties of the Agda language. The result of this scope checking pass is a correct by construction AST that contains a proof that the syntax is well-scoped represented as paths from references of names (eg. x) to declarations (eg. x = ...).