@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"
}