Sciweavers

Share
ENTCS
2007

A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F

8 years 7 months ago
A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F
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 malization, 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 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. Key words: Logical frameworks, Normalization, Tait’s method, Logical relations, Reducibility candidates, HOAS, ATS/LF
Kevin Donnelly, Hongwei Xi
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Kevin Donnelly, Hongwei Xi
Comments (0)
books