"An introduction to the Polymorphic Lambda Calculus" (John C. Reynolds)

citeseerから入手可能。今まで、職場関係の論文はBlogで取り上げなかったのですが、備忘を兼ねてこちらにのせることにしました。といっても、私は計算機科学に関してはド素人なので、あまり有益な情報提供はできないと思います。
この論文、本文が7ページで、証明等はありません。多相型λ計算についてその定義と、強い意味で正規化可能であることと、他に例えば不動点演算子を加えると正規化が保証できなくなるとか2種類のモデルがあるとかパラメトリシティに関しては分かってないことが多いとか、「誰がどんな結果を証明した」という基本事項をまとめてあります。参考文献リストが有益です。