Publication details

Saarland University Computer Science

A Proof of Strong Normalization for Call-by-push-value

Christian Doczkal, Jan Schwinghammer


The call-by-push-value (CBPV) calculus is a general framework within which one can study computational effects such as state, nondeterminism, and input/output. Compared to the simply typed lambda calculus, the CBPV type system is much more fine-grained and distinguishes between value and computation types. We give a self-contained proof of strong normalization for CBPV, employing a notion of TopTop-closure to adapt the Girard-Tait method to CBPV computation types.

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy