@article{SilesHerbelin11,
  author      = {Vincent Siles and Hugo Herbelin},
  title       = {Pure Type Systems conversion is always typable},
  journal     = {Journal of Functional Programming},
  publisher   = {Cambridge University Press},
  year        = {2012},
  volume      = {22},
  number      = {2},
  month       = {Mar},
  pages       = {153-180},
  doi         = {10.1017/S0956796812000044}
}