@article{CoquandHerbelin94,
  author      = {Thierry Coquand and Hugo Herbelin},
  title       = {A-Translation and Looping Combinators in Pure Type Systems},
  journal     = {Journal of Functional Programming},
  pages       = {77--88},
  publisher   = {Cambridge University Press}, 
  volume      = {4},
  number      = {1},
  year        = {1994},
  issn        = {0956-7968}
}