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

Into the depths of C: elaborating the de facto standards. - Kayvan Memarian; Justus Matthiesen; James Lingard; Kyndylan Nienhuis; David Chisnall; Robert N. M. Watson; Peter Sewell (PLDI, 2016)