Publication details

Saarland University Computer Science

Formalizing TT-lifting in Isabelle/HOL-Nominal

Christian Doczkal

Master's Thesis, Saarland University, June 2009

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.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy