Handling variable binding is one of the main difficulties in formal proofs. In this context, Moggi’s computational metalanguage serves as an interesting case study. It features monadic types and a commuting conversion rule that rearranges the binding structure. Lindley and Stark have given an elegant proof of strong normalization for this calculus. The key construction in their proof is a notion of relational ⊤⊤-lifting, using stacks of elimination contexts, to obtain a Girard-Tait style logical relation. We give a formalization of their proof in Isabelle/HOL-Nominal with a particular emphasis on the treatment of bound variables. Using the Isar structured proof language and the Isabelle document preparation system, we obtain a formal proof document that is suitable for human consumption.
Login to edit
Wed Sep 16 10:47:00 2009