Grading call-by-push-value, explicitly and implicitly

Conference item

We present call-by-push-value with effects (CBPVE), a refinement of Levy’s call-by-push-value (CBPV) calculus in which the types contain behavioural information about the effects of computations. CBPVE fits well into the existing literature on graded types and computational effects. We demonstrate this by providing graded call-by-value and call-by-name translations into CBPVE, and a semantics based on algebras for a graded monad. CBPVE is designed as a standalone calculus, with explicit grade information in the syntax. We use it to study the assignment of graded types to the terms of an ungraded calculus such as CBPV, essentially treating the grades as implicit. To interpret such terms in a model that accounts for the grades, one has to prove a coherence result for the implicit grades. We show that, in the case of a graded monadic semantics, the necessary coherence result is false in general. To solve this problem, we show that a mild condition on the algebra of grades is enough to guarantee coherence, giving the first proof of a coherence result for grading, and hence also the first graded monadic semantics for CBPV computations.

Authors: McDermott, D

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
• Host title: 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
• Volume: 337
• Pages: 28:1-28:19
• Article number: 28
• Series: Leibniz International Proceedings in Informatics (LIPIcs)
• Publication date: 2025-07-07
• Acceptance date: 2025-04-30
• Event title: 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
• Event location: Birmingham, UK
• Event website: https://fscd2025.github.io/
• Event start date: 2025-07-14
• Event end date: 2025-07-20
• DOI: 10.4230/LIPIcs.FSCD.2025.28
• ISBN: 9783959773744
• Language: English