Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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