# Publication details

##
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

@INPROCEEDINGS{Doczkal:Schwinghammer:09,
title = {Formalizing a Strong Normalization Proof for Moggi's Computational Metalanguage},
author = {Christian Doczkal and Jan Schwinghammer},
year = {2009},
publisher = {{ACM}},
booktitle = {4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'09)},
note = {{To appear}},
}

Login to edit

Legal notice, Privacy policy