Strong normalization is one of the fundamental proof-theoretic aspects of many typed lambda-calculi. We prove strong normalization of Call-By-Push-Value with respect to a small-step reduction relation based on the equational theory of the calculus. To obtain a uniform treatment of the various computation types of Call-By-Push-Value, we adapt Lindley's TT-lifting to a notion of TT-closure. This allows us to define a Girard/Tait style reducibility predicate, in the presence of several different computation types.
Download PDF Show BibTeX
Login to edit