Agda is a proof assistant based on Martin-Löf type theory. Its type theory and "implementation theory" were introduced by Ulf Norrell in 2007.
Its implementation is slightly different from Ulf's description. Apart from the large amount of extensions, the most notable difference is about universe levels. In Ulf's thesis, Agda has cumulative universes, but this is missing for more than 10 years until Jesper Cockx added it as an unsafe language extension.
The Agda wiki
Agda 2 was introduced in Ulf Norrell's thesis:
Norrell, Ulf. 2007. ‘Towards a Practical Programming Language Based on Dependent Type Theory’. PhD thesis, Chalmers University of Technology. https://research.chalmers.se/en/publication/46311.
@phdthesis{norrell_towards_nodate,
type = {{PhD} thesis},
date = {2007},
title = {Towards a practical programming language based on dependent type theory},
url = {https://research.chalmers.se/en/publication/46311},
school = {Chalmers University of Technology},
author = {Norrell, Ulf}
}