Publication details

Saarland University Computer Science

Formalizing a Strong Normalization Proof for Moggi's Computational Metalanguage

Christian Doczkal, Jan Schwinghammer

4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'09), ACM, 2009

Lindley and Stark have given an elegant proof of strong normalization for various lambda calculi whose type systems preclude a direct inductive definition of Girard-Tait style logical relations, such as the simply typed lambda calculus with sum types or Moggi's calculus with monadic computation types. The key construction in their proof is a notion of relational TT-lifting, which is expressed with the help of stacks of evaluation contexts. We describe a formalization of Lindley and Stark's strong normalization proof for Moggi's computational metalanguage in Isabelle/HOL, using the nominal package.

Theory file

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy