The Agda programming language, in version 2, has been developed at the Chalmers/GU Department of Computer Science and Engineering since 2006. It is a functional programming language with strong type system. Its dependent types allow the programmer to express strong data structure invariants and properties of programs, enabling a correct-by-construction programming style.
A common technique in programming language development is bootstrapping, i.e., implementing the new programming language in itself. This fuels the development process as there is a large example program from the beginning to stress-test the language implementation.
Agda is currently implemented in Haskell. A reimplementation of Agda in Agda would not only present a large use-case for dependently typed an correct-by-construction programming, it would also make the Agda implementation more principled and stable.
In this master thesis, the first compiler pass for Agda is to be developed in Agda. This first pass is the scope checker which transforms the abstract syntax tree produced by the parser into intrinsically well-scoped syntax trees. Such well-scoped trees will be statically guaranteed to have no invalid references to identifiers; the guarantee will be given by the dependent typing of these trees. As a side effect, the engineering of the type of well-scoped trees will likely lead to a more precise definition of the Agda language, clarifying unclear corner cases of the current implementation.
Suggested supervisor: Andreas Abel