An Agda scope checker implemented in Agda
Ladda ner
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2023
Författare
Gazzetta, Francesco
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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 = ...).
Beskrivning
Ämne/nyckelord
Computer science , Agda , compilers , scoping , well-scoped syntax , dependent types , name resolution , formal verification