Lindley and Stark have given an elegant proof of strong normalization for various lambda calculi whose type systems preclude a direct inductive definition of Girard-Tait style logical relations, such as the simply typed lambda calculus with sum types or Moggi's calculus with monadic computation types.
The key construction in their proof is a notion of relational TT-lifting, which is expressed with the help of stacks of evaluation contexts.
We describe a formalization of Lindley and Stark's strong normalization proof for Moggi's computational metalanguage in Isabelle/HOL, using the nominal package.
Download PDF Show BibTeX
Login to edit