Publication details

Saarland University Computer Science

Strong Normalization of Call-by-push-value

Christian Doczkal

B.Sc. Thesis, Programming Systems Lab, Department of Informatics, Saarland University, 2007

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


Webmaster, Wed Sep 16 10:47:00 2009