Inductive Type Schemas as Functors. - Freiric Barral; Sergei Soloviev 001 (CSR, 2006)

Decidability for non-standard conversions in typed lambda-calculi. - Freiric Barral (2008)