Email Gateway (Aug 18 2022 at 15:55): Email Gateway (Aug 18 2022 at 15:55):From: Tobias Nipkow <nipkow@in.tum.de>
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.
http://afp.sourceforge.net/entries/Lam-ml-Normalization.shtml
Last updated: Apr 19 2024 at 16:20 UTC