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