| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
project summary
Strong Normalization of Moggis's Computational Metalanguage
| Title: | Strong Normalization of Moggis's Computational Metalanguage |
| Author: | Christian Doczkal (doczkal /at/ ps /dot/ uni-saarland /dot/ de) |
| Submission date: | 2010-08-29 |
| Abstract: | 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. |
| BibTeX: |
@article{Lam-ml-Normalization-AFP,
author = {Christian Doczkal},
title = {Strong Normalization of Moggis's Computational Metalanguage},
journal = {Archive of Formal Proofs},
month = aug,
year = 2010,
note = {\url{http://afp.sf.net/entries/Lam-ml-Normalization},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is the development version, revision 4b34a59339a6, of this entry, generated for Isabelle revision 090a519982e9. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|