The Lisp in the Cellar: Dependent types that live upstairs [pdf]

Downloadable: https://zenodo.org/records/15424968/files/deputy-els.pdf