A Step-indexed Semantic Model of Types for the Call-by-Name Lambda Calculus

TL;DR

This paper introduces a generalized step-indexed semantic model for the call-by-name lambda calculus, enabling proof of type safety for general recursion, advancing semantic understanding of typed functional languages.

Contribution

It extends step-indexed models to call-by-name calculus and demonstrates type safety for recursive functions within this framework.

Findings

Successfully models call-by-name semantics with step-indexing.

Proves type safety for recursive functions in the model.

Provides a foundation for further semantic analysis of typed lambda calculi.

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.