Pith. sign in

REVIEW 3 major objections 4 minor 57 references

Package Managers \`a la Carte: A Formal Model of Dependency Resolution

T0 review · 3 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A three-rule calculus — root inclusion, dependency closure, version uniqueness — is claimed to capture the common core of all package managers, with each ecosystem-specific feature reduced to that core by sound and complete encodings.

desk verdict A promising unifying formalization of dependency resolution that needs full proofs for its reduction theorems and a more honest composition story before the 2n-translator claim is credible. read the letter →

arxiv 2602.18602 v5 pith:2GWZIIZF submitted 2026-02-20 cs.PL cs.SE

Ryan Gibb , Patrick Ferris , David Allsopp , Thomas Gazagnaire , Anil Madhavapeddy This is my paper · ORCID
classification cs.PLcs.SE
keywords PackageCalculusdependencyresolutionmanagersformalsemanticsreductionsconflictsconcurrentversionscross-ecosystemtranslation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper tries to establish that every package manager, however idiosyncratic, runs on a common three-rule core: the resolved set must include the root, must be closed under dependencies, and can contain only one version of any package name. It defines this core as the Package Calculus and then shows, extension by extension, that conflicts, concurrent versions, peer dependencies, features, package formulae, variable formulae, and virtual packages can all be encoded back into the core by adding synthetic packages with structured names. Each encoding is claimed to preserve valid resolutions exactly, so the reductions double as compilation passes: a dependency expression in any ecosystem can be lowered to the core, solved there, and lifted into another ecosystem. The payoff is that translating among n package managers needs 2n translators through the core rather than n² direct translators, which would let a multilingual project resolve OCaml, Rust, Python, and system dependencies in one pass and see the full dependency graph.

What carries the argument

The carrying object is the Package Calculus itself: a dependency relation from packages (name, version) to name-and-version-set, with validity defined by root inclusion, dependency closure, and version uniqueness. The mechanism that makes the extensions work is the synthetic package: each extension is encoded by injecting new packages with structured names, often two versions 0 and 1, and rewiring dependencies so that the core's version-uniqueness condition enforces the extension's constraint. Supporting sub-mechanisms include a granularity function that maps versions to coarse labels for concurrent versions, linear auxiliary packages that encode formula disjunction without exponential blowu

What would settle it

Concrete test: take a small instance of any extension, for example a package A that conflicts with versions 1 and 2 of B while also depending on C, and compare the set of valid resolutions under the extension with the set produced by the reduction to the core. If any reduction maps a satisfiable extended instance to an unsatisfiable core instance, or yields a core resolution that decodes to an invalid extended resolution, the central claim fails. A systematic version: enumerate all small repositories, encode both the extension and its reduction as SAT instances, and check satisfiability equiva

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is a unification result: dependency resolution in more than thirty surveyed package managers is not thirty different problems but one problem with optional vocabulary. The Package Calculus fixes a minimal semantics — root inclusion, dependency closure, version uniqueness — and the paper's reductions show this semantics is expressive enough to absorb the axes along which package managers diverge. Conflicts become synthetic packages with versions 0 and 1; concurrent versions push a granularity label into the package name; features become feature-labelled packages; disjunction and negation become auxiliary one-of-two packages; variables become packages ra

Load-bearing premise

The load-bearing premise is that every reduction in Sections 4.1 through 4.7 is sound and complete — that is, it neither creates nor destroys valid resolutions — but the paper states these theorems without supplying proofs; the only formal claim with a proof is the NP-completeness argument in Appendix B.

Editorial extensions

If this is right

  • Cross-ecosystem translation reduces to writing one lowerer and one lifter per ecosystem; a resolver built on the core can serve all of them.
  • A dependency graph spanning OCaml, Rust, Python, and system packages could be resolved as a single instance, making security-vulnerability analysis and SBOM generation see the full transitive closure.
  • New dependency constructs can be incorporated into the translation network as soon as they admit a sound and complete reduction to the core, without rewriting other ecosystems' translators.
  • The complexity spectrum is formalized: minimum-version-only constraints give linear-time resolution, removing version uniqueness gives greedy resolution, and full expressiveness is NP-complete.
  • Where reductions compose, they do so because encodings are version-preserving; where they do not compose, the paper specifies the ordering constraints or mutual awareness required.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the practical value of the 2n pipeline depends on the unproven soundness and completeness theorems; formalizing them in a proof assistant or finding a counterexample would be the natural next step.
  • Editorial inference: the encodings suggest a testable extension — generate random small dependency instances in two ecosystems, lower both to the core, and check that satisfiability and selected versions agree; disagreements would pinpoint where ecosystem semantics diverge.
  • Editorial inference: the calculus models resolution only, not deployment order or build semantics; a full cross-ecosystem tool would need to couple these with the build-graph treatment of optional dependencies.
  • Editorial inference: the NP-completeness of the core implies that cross-ecosystem resolution inherits exponential worst-case behavior; practical tools would need SAT-style engines, so this formalism is a semantic backbone rather than a performance recipe.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes the Package Calculus, a minimal three-rule formal system for dependency resolution (root inclusion, dependency closure, version uniqueness). It surveys over thirty package managers, identifies seven axes of semantic diversity (conflicts, concurrent versions, peer dependencies, features, package formulae, variable formulae, virtual packages), and defines an extension of the core calculus for each. The central claim is that every extension can be reduced to the core via sound and complete reductions, so that the core can serve as an intermediate representation reducing cross-ecosystem translation from n² to 2n translators. The paper proves NP-completeness of the core (Appendix B) and gives a SAT encoding (Appendix C), but the soundness/completeness theorems for the reductions are stated without proof. The composition of reductions is only proved informally for features plus concurrent versions, and §5.2.2 explicitly notes a conflict between the conflict/negation encodings and the concurrent-versions relaxation.

Significance. If the reductions and composition claims were fully proved, the Package Calculus would be a valuable unifying framework for package-manager semantics, with practical potential for cross-ecosystem dependency resolution and supply-chain analysis. The survey and taxonomy (§2, Table 1) are useful as a systematization of package-manager features, and the core calculus is clearly and precisely defined. The NP-completeness proof and the SAT encoding are solid contributions. However, the paper's central formal claims—the sound and complete reductions of all seven extensions and the 2n-translator pipeline—are currently unproved, and the paper itself identifies a load-bearing composition limitation. The framework is promising, but in its present form the formal results do not support the advertised conclusions.

major comments (3)
  1. [§4 (Theorems 4.1.4–4.1.5, 4.2.4–4.2.5, 4.3.4–4.3.5, 4.4.5–4.4.6, 4.5.5–4.5.6, 4.6.4–4.6.5, 4.7.4–4.7.5; also Theorem 3.2] All soundness and completeness theorems for the reductions are stated without proof. For example, Theorem 4.1.4 and Theorem 4.1.5 are essential to the claim that conflicts are faithfully modelled, yet no derivation is provided. The same applies to every other reduction in §4. The paper's central contribution is a set of formal equivalences; without proofs, these remain conjectures. The authors should supply full proofs for each theorem, or at least rigorous proof sketches that demonstrate the key invariants (e.g., why synthetic conflict packages cannot be bypassed, why intermediate packages preserve parent-relation uniqueness, and why feature unification is maintained).
  2. [§5.2.2 (Limits of Composition) and §5 (2n translator claim)] The paper claims that using the core as an IR reduces translation from n² to 2n translators, but this presupposes that combinations of extensions can be lowered by composing the reductions. The paper itself admits in §5.2.2 that the conflict reduction (Definition 4.1.3) and the package-formula negation encoding (Definition 4.5.4) rely on version uniqueness, which the concurrent-versions extension (Definition 4.2.2) relaxes. The suggested remedy—'reducing concurrent versions first'—is not accompanied by a combined reduction or a correctness theorem. Consequently, the 2n claim is unsupported for ecosystems that combine concurrent versions with conflicts, such as Portage (slots and blockers) or any future manager mixing these features. A general composition theorem, or an explicit and proved characterization of which extension combinations are composable, is needed before the pipeline claim
  3. [§5.2.1 (Theorems 5.2.2 and 5.2.3)] Even the one positive composition result—features with concurrent versions—is only supported by an informal argument ('the feature reduction is version-preserving') and the two theorems are stated without proof. This is the only fully worked composition in the paper, and it is central to the claim that the framework can handle real-world managers like Cargo. Please provide actual proofs for Theorems 5.2.2 and 5.2.3, or downgrade the presentation to a conjecture and clearly mark it as unproved.
minor comments (4)
  1. [Definition 4.1.2(b)] The conflict-avoidance condition contains a corrupted symbol ('šv∈vs') that should be the non-existence quantifier (e.g., ∄). Please fix the typo for readability.
  2. [§5.1 (Transpiling Pipeline)] The sentence 'Where the target ecosystem does not support an extension, the core encoding is emitted directly' is unclear. If the target DSL cannot express the extension natively, how can the core encoding with structured names like ⟨n,g(v)⟩ be emitted into that DSL? This needs a concrete explanation or an example.
  3. [Table 1] The footnote numbering is confusing: footnote 3 ('Limited support with ‘Slotting’') appears to annotate the 'Concurrent Versions' column for Portage, but the footnote marker is attached to the Toolchain column. Please align the markers with the intended cells.
  4. [Definition 4.5.4(b)(iv)] The De Morgan rule E(p ΔΨ ¬(ψL∧ψR)) = E(p ΔΨ ¬ψL∨¬ψR) introduces a disjunction that is not a syntactic subformula of the original; this is fine because the encoding is recursive, but the rule should be stated more carefully to avoid the impression that ΔΨ is closed under such rewriting.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: reductions are explicit encodings; the 2n-translator claim is an architectural consequence, not a fitted or self-cited prediction.

full rationale

I walked the claimed derivation chain. The core calculus (Def 3.1.3) is defined independently; the version-formula reduction (Def 3.2.6) expands each formula to its denotation from Def 3.2.3, so Thm 3.2.7 is a definitional equivalence, but it is a reduction in the intended formal sense, not a prediction forced by fitting. Each extension in §4 (conflicts, granularity/concurrent versions, peer dependencies, features, package formulae, variable formulae, virtual packages) is introduced with its own definitions, and each reduction is an explicit syntactic encoding into the core via synthetic package names/versions (e.g., Conflict Reduction Def 4.1.3, Package Formula Reduction Def 4.5.4), with witness-set constructions in the completeness directions. No parameter is calibrated from data and no target quantity is used to define the input objects. The 2n-translator claim (§5) is a hub-and-spoke architectural consequence of using the core as an intermediate representation, not an empirical output already contained in the inputs. The paper itself flags the composition limitation: §5.2.2 states that the conflict reduction and the negation encoding both introduce synthetic packages with two versions whose mutual exclusion relies on core version uniqueness, and that relaxing version uniqueness to version granularity 'allowing both versions to coexist and breaking the encoding.' This is a real limitation and means the 2n-claim is not fully established for combined extensions, but it is an omitted composition theorem, not circularity. The soundness/completeness theorems 4.1.4–4.7.5 are stated without proofs; that is a verification gap and would make the pipeline unsound if false, but it is not a circular step. I found no load-bearing self-citation: no prior result by these authors is invoked to justify the core or to forbid alternatives. Hence score 0.

Assumptions & free parameters 3 free parameters · 3 assumptions · 7 invented entities

The model is abstract and introduces no physical entities; the invented entities are all synthetic package-name encodings internal to the reductions. Free parameters are ecosystem-specific inputs (granularity function, version ordering, variable assignment). The central formal claim rests on unproven soundness/completeness theorems, which are listed as axioms of the argument.

free parameters (3)
  • granularity function g = per-ecosystem: e.g., semver major for Cargo, identity for npm/Nix, ε for single-version
    Definition 4.2.1 introduces g: V→G without constraints; the reduction to core (Definition 4.2.3) uses W={g(u)|u∈vs} as a version set, implicitly requiring G⊆V. The choice of g determines which concurrent versions are allowed.
  • version ordering ≤v = per-ecosystem
    Definition 3.2.1 takes an arbitrary total order on versions as input; the ordered SAT encoding (Appendix C) relies on this order to prioritize versions.
  • variable assignment σ = variable (e.g., os-distribution, arch)
    Definition 4.6.1 treats the assignment σ as part of the model, not derived from the calculus; the Variable Formula reduction (Definition 4.6.3) depends on σ's values.
assumptions (3)
  • standard math Sets, relations, total order, and NP-completeness of 3-SAT (Cook-Levin)
    The NP-completeness proof (Theorem 3.1.4, Appendix B) relies on the well-known NP-completeness of 3-SAT and standard set-theoretic constructions.
  • domain assumption Version sets are finite or explicitly representable
    Definition 3.2.6 evaluates version formulae to finite sets of versions; the reduction to core assumes such sets can be materialized. In practice repositories are finite, but the formalism does not state this.
  • domain assumption Granularity values are themselves versions (G⊆V)
    Definition 4.2.3 uses W={g(u)|u∈vs} as a version set for intermediate packages; this requires g(u)∈V. The paper does not state this constraint explicitly.
invented entities (7)
  • Synthetic conflict packages ⟨n,vs⟩ with versions 0 and 1
    purpose: Encode conflicts via version uniqueness in the core calculus
    Definition 4.1.3 introduces packages named ⟨n,vs⟩ with two versions to enforce mutual exclusion; these have no meaning outside the reduction.
  • Granularity-renamed packages ⟨n,g(v)⟩
    purpose: Encode concurrent versions by pushing granularity into the package name
    Definition 4.2.3 renames each package to ⟨n,g(v)⟩ so that version uniqueness in the core enforces the granularity constraint.
  • Intermediate packages ⟨n,v,m⟩
    purpose: Encode dependencies that split across multiple granularity versions and peer dependencies
    Definitions 4.2.3 and 4.3.3 introduce intermediate packages that connect a depender to a specific subset of versions; they are purely internal artifacts.
  • Feature packages ⟨n,f⟩
    purpose: Encode features by turning each feature-selected package into a distinct package name
    Definition 4.4.4 creates ⟨n,f⟩ packages to represent feature selections while preserving version uniqueness.
  • Variable packages ⟨g⟩ and ⟨p,l⟩
    purpose: Encode global and local variables as package names in the core
    Definition 4.6.3 turns each variable value into a package so that variable satisfaction can be checked by dependency closure.
  • Virtual provider intermediates ⟨p,n⟩ with versions ⟨m,w⟩
    purpose: Encode virtual packages by selecting a unique provider through version uniqueness
    Definition 4.7.3 creates intermediate packages whose versions correspond to potential providers, forcing a single provider choice.
  • Auxiliary disjunction packages ⟨ψL∨ψR⟩ with versions 0/1
    purpose: Encode boolean package formulae via a Tseitin-style encoding
    Definition 4.5.4 introduces synthetic packages for each disjunction to keep the reduction linear in formula size.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Package Managers \`a la Carte: A Formal Model of Dependency Resolution." pith.science (2026). https://pith.science/paper/2GWZIIZF

@misc{pith2026260218602,
  author       = {Pith},
  title        = {Pith review of: Package Managers \`a la Carte: A Formal Model of Dependency Resolution},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2GWZIIZF}},
  note         = {Machine review of arXiv:2602.18602}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2602.18602 by the authors.

Figure 1
Figure 1. An instance of the Package Calculus. 3.2 Versions We express a dependency on an abstract set of compatible versions (Definition 3.1.2), which is normally expressed with a version formula – relational and logical expressions defining compatible version sets. To support version formulae, package managers typically impose a non-lexicographical total ordering of versions. Definition 3.2.1 (Version Ordering). A version o… view at source ↗
Figure 2
Figure 2. Conflict Package Calculus (𝐴, 1)Γ(𝐵, {1, 2}) reduced to the core calculus. Definition 4.1.3 (Conflict Reduction). Given 𝑅Γ, ΔΓ, 𝑟Γ, and Γ, we define a reduction to the core calculus with 𝑅, Δ, and 𝑟, as follows: (a) Packages: 𝑟 = 𝑟Γ and 𝑅 = 𝑅Γ ∪ Ð 𝑝Γ(𝑛,𝑣𝑠 ) {(⟨𝑛, 𝑣𝑠⟩, 0) , (⟨𝑛, 𝑣𝑠⟩, 1)} where ⟨𝑛, 𝑣𝑠⟩ ∈ 𝑁 (b) Dependencies: Δ = ΔΓ ∪ Ø 𝑝Γ(𝑛,𝑣𝑠 ) [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Dependencies exhibiting the ‘diamond dependency problem’. [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: Concurrent Package Calculus dependencies where [PITH_FULL_IMAGE:figures/full_fig_p013_4.png]
Figure 5
Figure 5. Figure 5: Reduction of Figure [PITH_FULL_IMAGE:figures/full_fig_p013_5.png]
Figure 6
Figure 6. Figure 6: Peer Package Calculus where parent 𝐴 depends on child 𝐵 with a peer dependency on 𝐶 and 𝑔(𝑣) = 𝑣. Definition 4.3.3 (Peer Dependency Reduction). Given 𝑅𝐶, Δ𝐶, Θ,𝑟𝐶, and 𝑔, we define a reduction to the core calculus with 𝑅, Δ, and 𝑟, as follows: (a) Packages: (i) ∀ (𝑛, 𝑣…
Figure 7
Figure 7. Figure 7: Feature Package Calculus instance. Definition 4.4.4 (Feature Reduction). Given 𝑅𝑓 , Δ𝑓 , Δ𝑎, 𝑠𝑢𝑝𝑝𝑜𝑟𝑡, and 𝑟𝑓 , we define a reduction to the core calculus with 𝑅, Δ, and 𝑟 as follows: (a) Packages: (i) 𝑟 = 𝑟𝑓 (ii) 𝑅 = 𝑅𝑓 ∪ {(⟨𝑛, 𝑓 ⟩, 𝑣) | (𝑛, 𝑣) ∈ 𝑅𝑓 , ( (𝑛, 𝑣), 𝑓 ) ∈ 𝑠…
Figure 8
Figure 8. Figure 8: Reduction of Figure [PITH_FULL_IMAGE:figures/full_fig_p017_8.png]
Figure 9
Figure 9. Figure 9: Concurrent Feature Package Calculus instance where [PITH_FULL_IMAGE:figures/full_fig_p023_9.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

57 extracted references · 7 canonical work pages

  1. [1]

    Comprehensive Perl Archive Network

    1995. Comprehensive Perl Archive Network. https://www.cpan.org/

    1995

  2. [2]

    OCaml Package Manager, The opam manual

    2013. OCaml Package Manager, The opam manual. https://opam.ocaml.org/doc/Manual.html

    2013

  3. [3]

    The Cargo Book

    2024. The Cargo Book. https://doc.rust-lang.org/cargo/

    2024

  4. [4]

    Cargo Resolver

    2024. Cargo Resolver. https://github.com/rust-lang/cargo/blob/15fbd2f607d4defc87053b8b76bf5038f2483cf4/src/cargo/ core/resolver/mod.rs

    2024

  5. [5]

    Debian Policy Manual: Chapter 5 - Control files and their fields

    2024. Debian Policy Manual: Chapter 5 - Control files and their fields. https://www.debian.org/doc/debian-policy/ch- controlfields.html

    2024

  6. [6]

    Debian Policy Manual: Chapter 7 - Declaring relationships between packages

    2024. Debian Policy Manual: Chapter 7 - Declaring relationships between packages. https://www.debian.org/doc/ debian-policy/ch-relationships.html

    2024

  7. [7]

    Go Modules Reference

    2024. Go Modules Reference. https://go.dev/ref/mod

    2024

  8. [8]

    The Haskell Cabal

    2024. The Haskell Cabal. https://www.haskell.org/cabal/

    2024

Show all 57 references
  1. [9]

    Pietro Abate, Roberto Di Cosmo, Georgios Gousios, and Stefano Zacchiroli. 2020. Dependency Solving Is Still Hard, but We Are Getting Better at It. In2020 IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER). 547–551. doi:10.1109/SANER482...

    2020

  2. [10]

    aboutcode-org. 2024. univers: a library for parsing and comparing software package versions and version ranges. https://github.com/aboutcode-org/univers

    2024

  3. [11]

    Jean-François Abramatic, Roberto Di Cosmo, and Stefano Zacchiroli. 2018. Building the universal archive of source code.Commun. ACM61, 10 (Sept. 2018), 29–31. doi:10.1145/3183558

    2018 doi

  4. [12]

    Snorri Agnarsson and M. S. Krishnamoorthy. 1985. Towards a theory of packages.ACM SIGPLAN Notices20, 7 (June 1985), 117–130. doi:10.1145/17919.806833

    1985

  5. [13]

    Mahmoud Alfadel, Diego Elias Costa, and Emad Shihab. 2023. Empirical analysis of security vulnerabilities in Python packages.Empirical Software Engineering28, 3 (March 2023). doi:10.1007/s10664-022-10278-4

    2023 doi

  6. [14]

    Mahmoud Alfadel, Diego Elias Costa, Emad Shihab, and Bram Adams. 2023. On the Discoverability of npm Vulnerabil- ities in Node.js Projects.ACM Trans. Softw. Eng. Methodol.32, 4, Article 91 (May 2023), 27 pages. doi:10.1145/3571848 Package Managers à la Carte -

    2023 doi

  7. [15]

    Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, and Ralf Treinen. 2022. The CoLiS platform for the analysis of maintainer scripts in Debian software packages.International Journal on Software Tools for Technology Transfer24, 5 (Sept. 2...

    2022 doi

  8. [16]

    Jon Bentley. 1986. Programming pearls: little languages.Commun. ACM29, 8 (Aug. 1986), 711–721. doi:10.1145/6424. 315691

    1986 doi

  9. [17]

    1970.Graphes et hypergraphes

    Claude Berge. 1970.Graphes et hypergraphes. Dunod, Paris, France

    1970

  10. [18]

    Aarnav M. Bos. 2023. A Review of Attacks Against Language-Based Package Managers. doi:10.48550/ARXIV.2302.08959

    2023 doi arXiv

  11. [19]

    Justin Cappos, Justin Samuel, Scott Baker, and John H. Hartman. 2008. A look in the mirror: attacks on package managers. InProceedings of the 15th ACM Conference on Computer and Communications Security(Alexandria, Virginia, USA)(CCS ’08). Association for Computing Machinery, N...

    2008

  12. [20]

    Paul Chiusano and Rúnar Bjarnason. 2020. Unison: A friendly programming language from the future. https: //www.unison-lang.org/

    2020

  13. [21]

    Serena Cofano, Giacomo Benedetti, and Matteo Dell’Amico. 2024. SBOM Generation Tools in the Python Ecosystem: an In-Detail Analysis. doi:10.48550/ARXIV.2409.01214

    2024 doi arXiv

  14. [22]

    Stephen A. Cook. 1971. The complexity of theorem-proving procedures. InProceedings of the Third Annual ACM Symposium on Theory of Computing(Shaker Heights, Ohio, USA)(STOC ’71). Association for Computing Machinery, New York, NY, USA, 151–158. doi:10.1145/800157.805047

    1971

  15. [23]

    Ludovic Courtès. 2013. Functional package management with guix.arXiv preprint arXiv:1305.4584(2013)

    2013 arXiv

  16. [24]

    2016.Version SAT

    Russ Cox. 2016.Version SAT. https://research.swtch.com/version-sat

    2016

  17. [25]

    Russ Cox. 2018. Go & Versioning: Minimal Version Selection. https://research.swtch.com/vgo-mvs

    2018

  18. [26]

    Roberto Di Cosmo. 2005. EDOS Deliverable WP2-D2.1: Report on Formal Management of Software Dependencies. https://hal.science/hal-00697463

    2005

  19. [27]

    Eelco Dolstra, Merijn de Jonge, and Eelco Visser. 2004. Nix: A Safe and Policy-Free System for Software Deployment. InProceedings of the 18th USENIX Conference on System Administration(Atlanta, GA)(LISA ’04). USENIX Association, USA, 79–92

    2004

  20. [28]

    Eelco Dolstra and Andres Löh. 2008. NixOS: a purely functional Linux distribution. InProceedings of the 13th ACM SIGPLAN International Conference on Functional Programming(Victoria, BC, Canada)(ICFP ’08). Association for Computing Machinery, New York, NY, USA, 367–378. doi:10....

    2008

  21. [29]

    Todd Gamblin, Massimiliano Culpo, Gregory Becker, and Sergei Shudler. 2022. Using Answer Set Programming for HPC Dependency Solving. InSC22: International Conference for High Performance Computing, Networking, Storage and Analysis. IEEE, 1–15. doi:10.1109/SC41404.2022.00040

    2022 arXiv

  22. [30]

    Collette, Gregory L

    Todd Gamblin, Matthew LeGendre, Michael R. Collette, Gregory L. Lee, Adam Moody, Bronis R. de Supinski, and Scott Futral. 2015. The Spack package manager: bringing order to HPC software chaos. InProceedings of the International Conference for High Performance Computing, Networ...

    2015

  23. [31]

    Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. 2011. Multi-Criteria Optimization in Answer Set Programming. InTechnical Communications of the 27th International Conference on Logic Programming (ICLP’11) (Leibniz International Proceedings in Informatics ...

    2011 doi

  24. [32]

    George D Greenwade. 1993. The comprehensive TEX archive network (ctan).TUGBoat14, 3 (1993), 342–351

    1993

  25. [33]

    Kurt Hornik. 2012. The comprehensive R archive network.Wiley interdisciplinary reviews: Computational statistics4, 4 (2012), 394–398

    2012

  26. [34]

    Paul Hudak. 1996. Building domain-specific embedded languages.ACM Comput. Surv.28, 4es (Dec. 1996), 196–es. doi:10.1145/242224.242477

    1996

  27. [35]

    Alexey Ignatiev, Mikoláš Janota, and Joao Marques-Silva. 2014. Towards efficient optimization in package management systems. InProceedings of the 36th International Conference on Software Engineering(Hyderabad, India)(ICSE 2014). Association for Computing Machinery, New York, ...

    2014

  28. [36]

    Peter Ivie and Douglas Thain. 2018. Reproducibility in Scientific Computing.ACM Comput. Surv.51, 3, Article 63 (July 2018), 36 pages. doi:10.1145/3186266

    2018 doi

  29. [37]

    Nandor Licker and Andrew Rice. 2019. Detecting Incorrect Build Rules. In2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE). 1234–1244. doi:10.1109/ICSE.2019.00125

    2019

  30. [38]

    Jiahuei Lin, Haoxiang Zhang, Bram Adams, and Ahmed E. Hassan. 2023. Vulnerability management in Linux distributions: An empirical study on Debian and Fedora.Empirical Software Engineering28, 2 (Feb. 2023). doi:10.1007/ s10664-022-10267-7

    2023

  31. [39]

    Christian Macho, Fabian Oraze, and Martin Pinzger. 2024. DValidator: An approach for validating dependencies in build configurations.Journal of Systems and Software209 (2024), 111916. doi:10.1016/j.jss.2023.111916 - Gibb et al

    2024

  32. [40]

    Andrey Mokhov, Neil Mitchell, and Simon Peyton Jones. 2018. Build systems a la carte. InInternational Conference on Functional Programming (ICFP’18). ACM. https://www.microsoft.com/en-us/research/publication/build-systems-la- carte/

    2018

  33. [41]

    Van-Hau Nguyen, Van-Quyet Nguyen, Kyungbaek Kim, and Pedro Barahona. 2021. Empirical Study on SAT-Encodings of the At-Most-One Constraint. InThe 9th International Conference on Smart Media and Applications(Jeju, Republic of Korea)(SMA 2020). Association for Computing Machinery...

    2021

  34. [42]

    package-url. 2024. vers: a mostly universal version range specifier. https://github.com/package-url/vers-spec

    2024

  35. [43]

    Pardis Pashakhanloo, Aravind Machiry, Hyonyoung Choi, Anthony Canino, Kihong Heo, Insup Lee, and Mayur Naik

  36. [44]

    Donald Pinckney, Federico Cassano, Arjun Guha, Jonathan Bell, Massimiliano Culpo, and Todd Gamblin. 2023. Flexible and Optimal Dependency Management via Max-SMT. In2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 1418–1429. doi:10.1109/ICSE4861...

    2023

  37. [45]

    Tom Preston-Werner. 2023. Semantic Versioning 2.0.0. https://semver.org/

    2023

  38. [46]

    pubgrub-rs contributors. 2020. pubgrub-rs: PubGrub version solving algorithm implemented in Rust. https://github. com/pubgrub-rs/pubgrub

    2020

  39. [47]

    Md Fazle Rabbi, Arifa Islam Champa, Costain Nachuma, and Minhaz Fahim Zibran. 2024. SBOM Generation Tools Under Microscope: A Focus on The npm Ecosystem. InProceedings of the 39th ACM/SIGAPP Symposium on Applied Computing(Avila, Spain)(SAC ’24). Association for Computing Machi...

    2024

  40. [48]

    Kristiina Rahkema and Dietmar Pfahl. 2022. Analysing the Relationship Between Dependency Definition and Updating Practice When Using Third-Party Libraries. InProduct-Focused Software Process Improvement, Davide Taibi, Marco Kuhrmann, Tommi Mikkonen, Jil Klünder, and Pekka Abra...

    2022

  41. [49]

    Martin Schwaighofer, Michael Roland, and René Mayrhofer. 2024. Extending Cloud Build Systems to Eliminate Transitive Trust. InACM Workshop on Software Supply Chain Offensive Research and Ecosystem Defenses (SCORED24) (Salt Lake City, Utah, USA). ACM

    2024

  42. [50]

    Jacob Stringer, Amjed Tahir, Kelly Blincoe, and Jens Dietrich. 2020. Technical Lag of Dependencies in Major Package Managers. In2020 27th Asia-Pacific Software Engineering Conference (APSEC). 228–237. doi:10.1109/APSEC51365.2020. 00031

    2020

  43. [51]

    1990.UNIX System V Release 4

    The UNIX System Group. 1990.UNIX System V Release 4. Programmer’s Guide: System Services and Application Packaging Tools. Prentice-Hall

    1990

  44. [52]

    Ralf Treinen and Stefano Zacchiroli. 2009. Common Upgradeability Description Format (CUDF) 2.0.The Mancoosi project (FP7)3 (2009). https://www.mancoosi.org/reports/tr3.pdf

    2009

  45. [53]

    G. S. Tseitin. 1970. On the Complexity of Derivation in Propositional Calculus. InStudies in Constructive Mathematics and Mathematical Logic, Part II, A. O. Slisenko (Ed.). Steklov Mathematical Institute, Leningrad, 115–125. Translated from Russian:Zapiski Nauchnykh Seminarov ...

    1970

  46. [54]

    Chris Tucker, David Shuffelton, Ranjit Jhala, and Sorin Lerner. 2007. Opium: Optimal package install/uninstall manager. In29th International Conference on Software Engineering (ICSE’07). IEEE, ACM, Minneapolis, MN, USA, 178–188

    2007

  47. [55]

    Natalie Weizenbaum. 2018. PubGrub: Next-Generation Version Solving. https://nex3.medium.com/pubgrub- 2fb6470504f

    2018

  48. [56]

    || ( ( =B-2 =C-1 ) ( =B-1 !!C ) )

    Lyuye Zhang, Chengwei Liu, Sen Chen, Zhengzi Xu, Lingling Fan, Lida Zhao, Yiran Zhang, and Yang Liu. 2023. Mitigating Persistence of Open-Source Vulnerabilities in Maven Ecosystem. In2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE). ACM/IEEE,...

    2023

  49. [2022]

    InProceedings of the 2022 ACM on Asia Conference on Computer and Communications Security(Nagasaki, Japan)(ASIA CCS ’22)

    PacJam: Securing Dependencies Continuously via Package-Oriented Debloating. InProceedings of the 2022 ACM on Asia Conference on Computer and Communications Security(Nagasaki, Japan)(ASIA CCS ’22). Association for Computing Machinery, New York, NY, USA, 903–916. doi:10.1145/348...

    2022

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.