This folder contains the Lean 4 mechanization of System Capless including its type soundness proof (Section 3 & 5 in the paper). This mechanized system also includes the scoped capabilities extension described in Section 5.2 of the paper, i.e., type soundness also implies scope safety.

The mechanization uses Lean version 4.21.0-rc3. If you compile from source, then Lean 4 needs to be installed on your system, which can be conveniently done with elan. The Lean manual also documents a way to quickly install Lean 4 with VSCode (see here). Alternatively, you can just explore through one of the virtual machine images we supplied, where everything is set up.

Navigate to the folder containing this README in a terminal and enter

make build

This will build and prove the metatheory of System Capless. The whole process takes a little bit under 2 minutes on an Apple M3 Pro Macbook Pro (32 GB RAM).

The virtual machine images also come with VSCode and the Lean 4 extension pre-configured. You can open the folder containing this mechanization from VSCode and start exploring.

Capless.lean is the entry file. Capless/Soundness/ contains the type soundness results.

The mechanization uses mathlib4 for basic data structures like Fin and aesop for automation.

Please refer to the top-level file Capless.lean for an overview of relevant Lean modules of the System Capless mechanization. The project can be inspected using the VSCode Lean extension, which is installed on the virtual machine images. We also provide a HTML documentation (see below).

The folder doc contains autogenerated html documentation from doc-gen4. To view it, navigate to that folder and invoke a local http server, e.g.,

 python3 -m http.server 8080

then open a browser and enter the URL localhost:8080.

This documentation can be (re-)generated by invoking

make doc

This will generate the documentation (that is outputed in the hidden folder .lake/build/doc) and copy it to the doc/ folder.

Note that doc-gen4 also includes the docs for all dependencies of this mechanization, such as mathlib4. During the building process, the tool will emit some warnings regarding those dependencies while generating the documentation. This is normal and can be safely ignored.

The top-level file dependencies.pdf visualizes the dependency graph among the mechanization's modules generated using the using the import-graph library. It can be (re-)generated by invoking

make graph

This section describes some important details of the mechanization and highlights the differences to the pencil and paper formalization.

The formalization is deBruijn-indexed and intrinsically-scoped. All syntactic categories in this mechanization are parameterized by the exact number of available binders in scope:

• Term n m k: A term in a context with n term variables, m type variables, and k capture variables
• CType n m k: A capturing type with the same indexing
• CaptureSet n k: A capture set in a context with n term variables and k capture variables
• Context n m k: A typing context defining exactly n, m, and k bindings respectively

Variable references use Fin n indices, ensuring that every variable reference is statically guaranteed to be within bounds. For example, in a Term 5 3 2, any term variable reference must be a Fin 5 (so between 0 and 4), any type variable reference must be a Fin 3, and any capture variable reference must be a Fin 2.

The key benefit is well-formedness by construction: it is impossible to construct ill-scoped terms, types, or capture sets. Traditional approaches require separate well-formedness predicates and must prove that operations preserve well-formedness. Here, well-formedness is by construction and there is no need for carrying through an additional predicate.

Both substitution and renaming lemmas are formulated using context morphisms, which provide a principled way to handle variable transformations while preserving typing relationships. The mechanization defines two families of context morphisms:

Renaming Morphisms (mapping bindings to bindings):

• VarMap Γ f Δ: Maps term variable bindings via function f : FinFun n n'
• TVarMap Γ f Δ: Maps type variable bindings via function f : FinFun m m'
• CVarMap Γ f Δ: Maps capture variable bindings via function f : FinFun k k'

Substitution Morphisms (mapping bindings to typing derivations):

• VarSubst Γ f Δ: Maps term variable bindings to typing judgments for Term.var (f x)
• TVarSubst Γ f Δ: Maps type variable bindings to subtyping relationships
• CVarSubst Γ f Δ: Maps capture variable bindings to appropriate subcapturing relationships

The key difference is that renaming morphisms (VarMap) map bindings to bindings (e.g., Γ.Bound x E → Δ.Bound (f x) (E.rename f)), while substitution morphisms (VarSubst) map bindings to typing derivations (e.g., Γ.Bound x E → Typed Δ (Term.var (f x)) (...)). Both families use FinFun for index-to-index mappings, but substitution morphisms produce the stronger guarantee of well-typed terms.

The substitution morphisms (VarSubst family) are used to prove traditional substitution theorems, such as showing that function application preserves typing when substituting arguments for parameters. Besides, the substitution morphism family builds upon and depends on the renaming morphism family (VarMap family).

The approach is inspired by techniques from Programming Language Foundations in Agda (PLFA), particularly the treatment of intrinsically-typed syntax and context morphisms.

The mechanization uses Full Monadic Normal Form for all syntactic categories. Unlike the paper presentation which applies MNF only to terms, this formalization extends MNF to types and capture sets as well:

• Type applications (Term.tapp) accept only type variables, not arbitrary type expressions
• Capture applications (Term.capp) accept only capture variables, not arbitrary capture sets
• Complex types and captures are bound as variables using Term.bindt and Term.bindc

For example, instead of writing x[{y,z}] directly, the MNF representation would be:

let c = {y,z} in x[c]

This design choice simplifies the metatheory: the only required transformation operation is renaming (mapping indices to indices), eliminating the need for complex substitution operations that replace variables with other syntactic objects (like types and capture sets).

The paper defines evaluation states as pairs ⟨σ | t⟩ where σ is a store and t is a term that decomposes into an evaluation context and redex t = e[u]. The mechanization refactors this representation into an explicit triplet ⟨σ | cont | t⟩ of type State n m k, where:

• σ : Store n m k is the store containing bindings and values,
• cont : Cont n m k is a continuation stack representing the evaluation context,
• t : Term n m k is the redex currently being evaluated.

This design makes the evaluation context explicit as a continuation stack. For example, the nested context let z2 = (let z1 = [] in t1) in t2 becomes a stack with continuation t1 followed by continuation t2, eliminating the need to syntactically decompose terms during evaluation.

The mechanization uses functional extensionality for etablishiing the equality between renaming functions.

The metatheory of System Capless is completely mechanized. There are no unfinished parts.