[isabelle] New AFP entry: Strong Normalization of Moggis's Computational Metalanguage

Christian Doczkal

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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.