Semantics and type checking of dependently-typed functional programs. - Yorck Hunke (2004)