Call-by-push-value
Paul Blain Levy
Abstract
Call-by-push-value (CBPV) is a form of typed λ-calculus that plays a fundamental role in the study of computational effects. This article is intended to be an accessible introduction. I thank Mike Mislove and SIGLOG for inviting me to expound one of my favourite subjects.
Topics & Concepts
FavouriteValue (mathematics)Computer scienceCalculus (dental)Political scienceLawDentistryMachine learningMedicineLogic, programming, and type systemsLogic, Reasoning, and KnowledgeFormal Methods in Verification