@inproceedings{AHS:95,
  pages = {182-199},
  title = {Categorical reconstruction of a reduction free normalization proof.},
  author = {T. Altenkirch and M. Hofmann and T. Streicher},
  publisher = {Springer},
  booktitle = {Proceedings of {CTCS}'95},
  year = {1995},
  volume = {953},
  series = {Lecture Notes in Computer Science},
}