@InProceedings{alti:types99,
  author = 	 {Andreas Abel and Thorsten Altenkirch},
  title = 	 {A Predicative Strong Normalisation Proof for a
                  $\lambda$-calculus with Interleaving Inductive Types},
  booktitle = 	 {{Types for Proof and Programs, International Workshop, TYPES '99, Selected Papers}},
  year =	 {2000},
  series =	 {Lecture Notes in Computer Science},
  volume =	 {1956},
  pages = "1--18"
}