@inproceedings{DonnellyXi06,
author = {Kevin Donnelly and Hongwei Xi},
title = {A Formalization of Strong Normalization for Simply Typed
Lambda-Calculus and System F},
booktitle = {Proceedings of Workshop on Logical Frameworks and Meta-Languages: Theory and Practice},
publisher = "ENTCS 174(5)",
pages = "109--125",
year = {2006},
location = {Seattle, Washington},
abstract = {{
We formalize in the logical framework ATS/LF a proof based on Tait's method
that establishes the simply typed lambda-calculus being strongly normalizing.
In this formalization, we employ higher-order abstract syntax to encode
lambda-terms and an inductive datatype to encode the reducibility predicate
in Tait's method. The resulting proof is particularly simple and clean
when compared to the previously formalized ones. Also, we mention briefly
how a proof based on Girard's method can be formalized in a similar fashion
that establishes System F being strongly normalizing.
}}
}