Strong Normalization of Moggis's Computational Metalanguage

Christian Doczkal 📧

August 29, 2010

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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 TT-lifting, using stacks of elimination contexts to obtain a Girard-Tait style logical relation. I give a formalization of their proof in Isabelle/HOL-Nominal with a particular emphasis on the treatment of bound variables.


BSD License


Session Lam-ml-Normalization