Package Managers à la Carte: A Formal Model of Dependency Resolution
Ryan Gibb, Patrick Ferris, David Allsopp, Thomas Gazagnaire, Anil Madhavapeddy
cs.PL
Feb 20, 2026 · v5
cs.SE
TL;DR
The Package Calculus's theorems, including the soundness of its reductions from extensions to the core calculus, are mechanised in Lean 4, with the artifact archived on Zenodo.
Abstract
Package managers are legion. Every programming language and operating system has its own solution, each with subtly different semantics for dependency resolution. This fragmentation prevents multilingual projects from expressing precise dependencies across language ecosystems; it leaves external system dependencies implicit and unversioned; and it obscures the full dependency graph that supply-chain analysis depends on. We present the Package Calculus, a formalism for dependency resolution that unifies the core semantics of package managers. Through a series of formal reductions, we show how this core is expressive enough to model the diversity of real-world dependency expression languages. The calculus provides the theoretical foundation for future cross-ecosystem tooling, as a lingua franca of dependency expression.
Problem
Package managers across language and OS ecosystems use subtly different dependency-resolution semantics. This fragmentation blocks precise cross-ecosystem dependencies and hides the full dependency graph from supply-chain analysis.
Approach
A survey of over thirty package managers identifies a shared core, which is formalised as the Package Calculus. Valid resolutions are defined by root inclusion, dependency closure, and version uniqueness. Extensions for conflicts, concurrent versions, peer dependencies, features, package and variable formulae, and virtual packages are each reduced back to the core by polynomial-time reductions with soundness theorems. The theorems are mechanised in Lean 4.
Results
The core calculus is expressive enough to model each of these axes of divergence, and the extensions compose to model real package managers. This supports polyglot resolution and translation between ecosystems through the core as an intermediate representation, replacing n^2 direct translators with 2n reductions and liftings.
