A Dependent Type Theory with Abstractable Names. - Andrew M. Pitts; Justus Matthiesen; Jasper Derikx (LSFA, 2014)