@phdthesis{luther:phd,
   author =  {Luther, Marko},
   title =   {Elaboration and Erasure in Type Theory},
   school =  {Universit{\"{a}}t Ulm},
   address = {Germany},
   year =    2003,
   url = {ftp://ftp.informatik.uni-ulm.de/pub/KI/papers/luther03-diss.pdf}}