The DOT (Dependent Object Types) calculus by Amin et al. (2016) is an ongoing effort to formalize the semantics of Scala, particularly abstract type members and path-dependent types.
This repository contains Agda translations of [https://github.com/amaurremi/dot-calculus](Rapoport et al.'s work) on the subject, particularly their simple proof of the calculus' soundness.