@InProceedings{alti:ctcs95,
  author =	 "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
  title =	 "Categorical reconstruction of a reduction free
		  normalization proof",
  year =	 "1995",
  booktitle = 	 "Category Theory and Computer Science",
  editor =	 {David Pitt and David E. Rydeheard and Peter Johnstone},
  series =	 {LNCS 953},
  pages =	 {182-199},
}