Typing Strictness

This repository contains a Rocq mechanization of the results described in the POPL 2026 paper: "Typing Strictness", and has been archived at Zenodo.

There are two options for reading this paper along with the code:

• The full paper (to be published at POPL 2026) will be linked here when it is available.
• The extended version of the paper is available on arXiv.

System requirements and build instructions

This code has been tested with The Coq Proof Assistant, version 8.18.0.

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

The proofs rely on two axioms: functional_extensionality_dep (Functional Extensionality) and Eqdep.Eq_rect_eq.eq_rect_eq (Axiom K). We use the former to work with Autosubst-style finite maps, while the latter is required by the dependent induction and dependent destruction tactics.

Mechanization overview

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

• autosubst2: Two files distributed with Autosubst 2. While we do not directly use Autosubst's tools in this mechanization, we do rely on the same primitives.

• common: Files used by all subsections. This includes the definition of and numerous lemmas about strictness attributes, along with some utility functions dealing with finite numbers.

• cbn: Definitions in Section 3 (CBN) and proofs about the CBPV->CBN translation (Section 4.5)

• cbpv : Definitions and Proofs in Section 4 (CBPV) and 5 (Semantic Properties)

• absence : Definitions and Proofs about the variant tracking unused variables (Section 6)

Claims

The paper makes a number of claims about the soundness of the CBPV language it describes, and the correctness of the translation between CBN and CBPV. The proofs of these claims are mechanized here.

• The fundamental_lemma lemma corresponds to Lemma 4.1.
• The soundness theorem corresponds to Theorem 4.2.
• The function_soundness theorem corresponds to Theorem 4.3.

Together, these theorems prove the type and attribute soundness of the CBPV language, and can be found in the soundness.v and semtyping.v files.

• The lemma translation_correct corresponds to Lemma 4.4.
• The theorem translation_correct_returner corresponds to Theorem 4.5.
• The theorem interpretation corresponds to Theorem 4.6.

Together, these three theorems prove the correctness of the translation from CBN to CBPV, and can be found in the translation.v file.

• The lazy_fundamental_lemma lemma corresponds to Lemma 5.1.
• The lazy_soundness theorem corresponds to Theorem 5.2.

These two theorems prove that the CBPV type system truly describes laziness, i.e., that the values of lazily used variables are never needed during evaluation. The proofs of these can be found in the soundness.v and lazy_semtyping.v files.

• The strict_fundamental_lemma lemma corresponds to Lemma 5.4.
• The strict_explosion theorem corresponds to Theorem 5.5.

These two theorems prove that the CBPV type system truly describes strictness, i.e., that the values of strictly used variables are definitely used during evaluation, or equivalently that a program missing a value for a strictly used variable will always fail. The proofs of these can be found in the soundness.v and strict_semtyping.v files.

Mechanization Details

The key difference between this development and the paper is that the paper presents a named version of the CBN and CBPV systems, while this mechanization uses de Bruijin indices. This difference is primarily noticeable in how scoping must be tracked in types and values: in a nameless setting it is not possible to compute the overlap between two arbitrary scopes. Instead, in the semantics of CBPV, values must be lowered when they move from a larger scope into a smaller one.

In particular, thunks and function closures track two scopes: mInner and mOuter. mInner is the scope of the actual computation inside the thunk or function, which is also the scope of the captured environment. The attribute vector captured by the thunk or function, however, is at mOuter scope, which represents the overlap that is computed in the named setting in the paper as part of the logical relations, but which we must track directly in the de Bruijn semantics. Whenever a value or computation terminal leaves a scope and enters a new one, we lower mOuter to the minimum of what it used to be and the height of the new scope. The new scope is equivalent to the scope that the typing judgment is viewing each term in, and so keeping track of mOuter this way will ensure that every thunk and closure "knows" which scope to use when computing the overlap between the scope of a type and the scope of the captured computation.

Development Structure

The development is organized as follows:

• The autosubst2 directory contains code inherited from the autosubst2 library for nameless de Bruijin variables. While this development does not directly use the code generation features of autosubst2, we do rely on many of its primitives.

• The common directory contains fintype.v, which contains a number of definitions and lemmas about finite numbers.

  • The attributes.v file contains the definitions for strictness attributes and vectors thereof, along with numerous lemmas about addition and comparison of attributes and vectors.
  • The definition attr_le defines the ordering on attributes found in the lattice in Figure 4.
  • The definition attr_stricter defines a different ordering on attributes by increasing strictness, and is used in the definitions in Figures 12 and 13.
  • The definition attr_add defines the addition operation on attributes found in Table 1.
  • The definition attr_vector_add defines the lifted version of attr_add on attribute vectors.
  • The definition attr_vector_le defines the lifted version of attr_le on attribute vectors.
  • The definition attr_vector_stricter defines the lifted version of attr_stricter on attribute vectors.
  • The definition lazyvector describes a vector that is Lazy for all variables.
  • The definition env_set (written γ <- q @ i) defines an operation that replaces one specific element in a vector with a different one. E.g., lazyvector <- Strict @ x is a vector that is lazy in all positions except for x. This is used in the definition of the variable rules for the typing and semantics.
  • The definition down_attrs and down_env_until define the vector lowering operation, written ↓γ in the paper, that is then lifted to types. This definition is also used implicitly in the semantics and in the logical relations as a means to restrict vectors to certain domains; checking that two attribute vectors γ and γ' agree on a common domain m is equivalent to checking whether down_env_until γ m H agrees with down_env_until γ' m H', where H and H' are proofs that m is indeed smaller than the actual lengths of γ and γ'.

• The cbn directory contains definitions and proofs about the CBN system.

  • The syntax.v file defines the syntax of types and terms, along with operations to rename and rescope them.
    • In particular, the operation down_ty corresponds to the ↓τ operation that drops a type into a lower scope.
  • The typing.v file defines typing contexts and the typing rules for CBN.
  • The translation.v file contains the definitions and proofs found in Section 4.5
    • The definitions translateType and translateContext correspond to the translation definitions found in Figure 11.
    • The definition translateTerm is the standard CBN term translation, also found in Figure 11.

• The cbpv directory contains definitions and proofs about the CBPV system.

  • The syntax.v file defines the syntax of types and terms, along with operations to rename and rescope them.
  • The typing.v file defines typing contexts and the typing rules for CBPV.
  • The renaming.v file contains proof that CBPV's typing judgment is stable under renamings, which is necessary for the proof of the correctness of the CBN-to-CBPV translation.
    • Note that because the types contain vectors, that is, functions of type fin n -> attr, autosubst cannot be used to generate the substitution and renaming lemmas, nor the actual renaming operations that are normally automatically generated. Instead, many of these are implemented manually here. However, these lemmas and definitions do not show up in any theorem statements, and are only used as helpers in the proof of translation_correct.
  • The semantics.v file contains definitions of CBPV's big step semantics, along with terminal values and environments. It also contains proofs that CBPV's semantics are deterministic-up-to-attributes.
    • The definitions eq_up_to_attrs and eq_env_up_to_attrs correspond to Figure 14 in the paper.
    • The definitions EvalValFail and EvalCompFail correspond to Definition 5.3 in the paper.
  • The semtyping.v file contains definitions and lemmas for the soundness proof in Section 4.4.
    • The definition LR corresponds to the logical relation in Figure 10 in the paper.
    • ρ_ok, SemVWt and SemCWt correspond to the definitions of semantic typing in Figure 10.
  • The lazy_semtyping.v file contains definitions and lemmas for the proof in Section 5.1.
    • The definition LR corresponds to the logical relation defined in Figure 12.
    • The definitions ρ_ok, SemVWt and SemCWt correspond to the definitions in Figure 13.
  • The strict_semtyping.v file contains the definitions and lemmas for the proof in Section 5.2.
    • The definitions LRM, LR_maybe, and LR_no correspond to the definitions in Figure 5.
    • The definitions ρ_not_ok, ρ_maybe_ok, SemVWt and SemCWt correspond to the definitions in Figure 16.
  • The soundness.v file contains the main top-level theorems and lemmas for CBPV.

• The absence directory contains a mirror of the rest of the development, except with the definition of attributes changed to include a 4th attribute tracking variables that are entirely unused, as described in Section 6.