A Step-indexed Semantic Model of Types for the Call-by-Name Lambda Calculus
Programming Languages
2011-05-17 v3
Abstract
Step-indexed semantic models of types were proposed as an alternative to purely syntactic safety proofs using subject-reduction. Building upon the work by Appel and others, we introduce a generalized step-indexed model for the call-by-name lambda calculus. We also show how to prove type safety of general recursion in our call-by-name model.
Keywords
Cite
@article{arxiv.1105.1985,
title = {A Step-indexed Semantic Model of Types for the Call-by-Name Lambda Calculus},
author = {Benedikt Meurer},
journal= {arXiv preprint arXiv:1105.1985},
year = {2011}
}
Comments
5 pages, 6 figures