Effects and Coeffects in Call-by-Push-Value

This repository contains a Coq mechanization of the results described in the OOPSLA 2024 paper: "Effects and Coeffects in Call-By-Push-Value". and has been archived at Zenodo.

We provide two options for connecting the paper with this code base.

Paper, with hyperlinks is the published version and contains hyperlinks that direct to the appropriate source file in this repository. This is a local copy of https://doi.org/10.1145/3689750.
Extended version of paper, with footnotes is an extended version of the paper that includes the full figures and contains footnotes to indicate the appropriate source file and definition. This is a local copy of https://arxiv.org/abs/2311.11795.

System requirements and build instructions

This code has been tested with The Coq Proof Assistant, version 8.19.2. The development requires the Autosubst 2 tool to regenerate the syntax files, but these syntax files are included in the distribution and do not need to be recreated.

The proofs can be compiled using the make command from the toplevel directory.

NOTE: The Makefile commands make and make clean will not regenerate or remove the generated syntax files; make fullmake and make fullclean will do so and so require Autosubst 2.

For tool installation help see artifact-creation.md. Alternatively, the Zenodo archive contains a virtual machine.

Mechanization overview

This mechanization is broken into several subdirectories corresponding to individual sections of the paper.

autosubst2: Two files distributed with Autosubst 2. These files have been slightly edited to make them compatible with Coq 8.19.0.
common: Files used by all subsections. This includes the axiomatizations for the effects and coeffect structures as well as an additional library for working with bounded natural numbers.
effects: Results in Section 2 (Effects)
general : Results in Section 3 (Coeffects, Version 1)
resource : Results in Section 4 (Coeffects, Version 2)
full: Results in Section 5 (Combined system)

Proof structure

The proofs include multiple base languages (CBPV, CBN, CBV) with multiple type systems (effects/general coeffects/resource coeffects/combined). In general, we use the following abbreviations for the base languages:

CBPV = Call-By-Push-Value
CBN = Call-By-Name lambda-calculus
CBV = Call-By-Value lambda-calculus
EffCBV = Call-By-Value lambda-calculus with effect tracking

Each language has its own version of some subset of the following files:

syntax.sig : Autosubst definition of the syntax
syntax.v : Definition of syntax, generated by Autosubst 2
typing.v : Typing rules
semantics.v : Big-step, environment-based operational semantics
semtyping.v : Definition of the logical relation and "semantic" typing rules (i.e. lemmas about the logical relation that mirror the typing rules)
soundness.v : Fundamental theorem of the logical relation, plus corollaries
renaming.v : Typing judgment stable under variable renaming
translation.v : Definition of a translation from the language to CBPV
proofs.v : Proofs that the translation preserves types

Required Axioms and assumptions

As this work uses Autosubst 2, we assume functional extensionality. We also use this axiom in the soundness proofs.

Functional extensionality (autosubst2/axioms.v)

For flexibility this development axiomatizes the required properties of the effect and coeffect structures used by the type systems and operational semantics.

Axiomatization of effects (common/effects.v)
Axiomatization of coeffects (common/coeffects.v)
Additional resource-tracking-specific axiomatization of coeffects (common/resource_axioms.v)
Axiomatization of discardable effects (common/junk_axioms.v)

Syntax overview

In each case, the syntax of the language has been generated using the Autosubst 2 tool, which represents variable binding using de Bruijn indices. Each syntactic form is indexed by a natural number (the scoping depth). The variable constructor uses a bounded natural number (fin n) as a index to ensure that all variable references are in scope.

We use the metavariables V and M for the syntax of CBPV values (Val n) and computations (Comp n) and A and B for CBPV value types (ValTy) and computation types (CompTy).

We use the metavariables e for lambda calculus terms (Tm n) and T for lambda calculus types (Ty).

Typing contexts (Γ) and environments (ρ) are represented as functions from variable indices (fin n) to types and values. These functions can only be applied to variables that are currently in scope. The cons infix operation .: extends a function to a larger scope.

Effects are notated by the metavariable ϕ; the identity effect is ϵ and effects can be combined with the infix operator E+ and compared using the infix predicate E<=.

Coeffects are notated by the metavariable q, with identity elemetnts Qzero and Qone. Individual coeffects can be compared with Qle, added with Qadd and multiplied with Qmult.

A sequence of coeffects is a grade vector γ, which can be added pointwise with Q+, multiplied by a single coeffect with Q*, and compared pointwise with Q<=. Grade vectors can also be extended using the infix notation .:. The notation 0s creates a grade vector containing only Qzero elements.

plclub/cbpv-effects-coeffects