A Formalized Proof of Strong Normalization for Guarded Recursive Types.

Andreas Abel, Andrea Vezzosi

Browse the full APLAS paper archive.