arXiv subjects

Patrick Ferris

Publications and source records attributed to Patrick Ferris.

7 recordsLinked to original sources

arXiv2026

Decomposable Type Highlighting for Bidirectional Type and Cast System

We explore how to provide programmers with an interactive interface for explaining the process by which static types and dynamic casts are derived, with the goal of improving the debugging of static and dynamic type errors. To this end, we define mathematical foundations for a decomposable highlighting system within a bidirectional system and show how these can be propagated through dynamic types in a cast system. Our prototype implementation in the gradually typed Hazel language includes a web-based user interface, through which we highlight the importance of type-level debugging.

cs.PL↗

arXiv2026

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

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.

cs.PL↗

arXiv2025

Emission Impossible: privacy-preserving carbon emissions claims

Information and Communication Technologies (ICT) have a significant climate impact, and data centres account for a large proportion of the carbon emissions from ICT. To achieve sustainability goals, it is important that all parties involved in ICT supply chains can track and share accurate carbon emissions data with their customers, investors, and the authorities. However, businesses have strong incentives to make their numbers look good, whilst less so to publish their accounting methods along with all the input data, due to the risk of revealing sensitive information. It would be uneconomical to use a trusted third party to verify the data for every report for each party in the chain. As a result, carbon emissions reporting in supply chains currently relies on unverified data. This paper proposes a methodology that applies cryptography and zero-knowledge proofs for carbon emissions claims that can be subsequently verified without the knowledge of the private input data. The proposed system is based on a zero-knowledge Succinct Non-interactive ARguments of Knowledge (zk-SNARK) protocol, which enables verifiable emissions reporting mechanisms across a chain of energy suppliers, cloud data centres, cloud services providers, and customers, without any company needing to disclose commercially sensitive information. This allows customers of cloud services to accurately account for the emissions generated by their activities, improving data quality for their own regulatory reporting. Cloud services providers would also be held accountable for producing accurate carbon emissions data.

cs.CR↗

arXiv2025

Solving Package Management via Hypergraph Dependency Resolution

Package managers are everywhere, with seemingly every language and operating system implementing their own solution. The lack of interoperability between these systems means that multi-lingual projects are unable to express precise dependencies across language ecosystems, and external system and hardware dependencies are typically implicit and unversioned. We define HyperRes, a formal system for describing versioned dependency resolution using a hypergraph that is expressive enough to model many ecosystems and solve dependency constraints across them. We define translations from dozens of existing package managers to HyperRes and comprehensively demonstrate that dependency resolution can work across ecosystems that are currently distinct. This does not require users to shift their choice of package managers; instead, HyperRes allows for the translation of packaging metadata between ecosystems, and for solving to be precisely specialised to a particular deployment environment.

cs.SE↗

arXiv2025

Steps towards an Ecology for the Internet

The Internet has grown from a humble set of protocols for end-to-end connectivity into a critical global system with no builtin "immune system". In the next decade the Internet will likely grow to a trillion nodes and need protection from threats ranging from floods of fake generative data to AI-driven malware. Unfortunately, growing centralisation has lead to the breakdown of mutualism across the network, with surveillance capitalism now the dominant business model. We take lessons from from biological systems towards evolving a more resilient Internet that can integrate adaptation mechanisms into its fabric. We also contribute ideas for how the Internet might incorporate digital immune systems, including how software stacks might mutate to encourage more architectural diversity. We strongly advocate for the Internet to "re-decentralise" towards incentivising more mutualistic forms of communication.

cs.NI↗

arXiv2024

Global, robust and comparable digital carbon assets

Carbon credits purchased in the voluntary carbon market allow unavoidable emissions, such as from international flights for essential travel, to be offset by an equivalent climate benefit, such as avoiding emissions from tropical deforestation. However, many concerns regarding the credibility of these offsetting claims have been raised. Moreover, the credit market is manual, therefore inefficient and unscalable, and non-fungible, therefore illiquid. To address these issues, we propose an efficient digital methodology that combines remote sensing data, modern econometric techniques, and on-chain certification and trading to create a new digital carbon asset (the PACT stablecoin) against which carbon offsetting claims can be transparently verified. PACT stablecoins are produced as outputs from a reproducible computational pipeline for estimating the climate benefits of carbon offset projects that not only quantifies the CO2 emissions involved, but also allows for similar credits to be pooled based on their co-benefits such as biodiversity and jurisdictional attributes, increasing liquidity through fungibility within pools. We implement and evaluate the PACT carbon stablecoin on the Tezos blockchain, which is designed to facilitate low-cost transactions while minimizing environmental impact. Our implementation includes a contract for a registry for tracking issuance, ownership, and retirement of credits, and a custodian contract to bridge on-chain and off-chain transactions. Our work brings scale and trust to the voluntary carbon market by providing a transparent, scalable, and efficient framework for high integrity carbon credit transactions.

cs.CR↗

arXiv2023

Planetary computing for data-driven environmental policy-making

We make a case for "planetary computing" -- infrastructure to handle the ingestion, transformation, analysis and publication of global data products for furthering environmental science and enabling better informed policy-making. We draw on our experiences as a team of computer scientists working with environmental scientists on forest carbon and biodiversity preservation, and classify existing solutions by their flexibility in scalably processing geospatial data, and also how well they support building trust in the results via traceability and reproducibility. We identify research gaps in the intersection of computing and environmental science around how to handle continuously changing datasets that are often collected across decades and require careful access control rather than being fully open access.

cs.DC↗