MobilityReadingGroup

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

Dylan MCDERMOTT

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 of 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.

@inproceedings{M2025,
  author = {Dylan McDermott},
  title = {{Grading call-by-push-value, explicitly and implicitly}},
  booktitle = {10th International Conference on Formal Structures for Computation and Deduction, 2025, Birmingham, UK},
  pages = {--},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{"{u}}r Informatik},
  year = 2025
}

@inproceedings{M2025,
  author = {Dylan McDermott},
  title = {{Grading call-by-push-value, explicitly and implicitly}},
  booktitle = {10th International Conference on Formal Structures for Computation and Deduction, 2025, Birmingham, UK},
  pages = {--},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{"{u}}r Informatik},
  year = 2025
}