arXiv subjects

Nikos Karayannidis

Publications and source records attributed to Nikos Karayannidis.

3 recordsLinked to original sources

arXiv2026

Pipeline Denotational Design: Correct-by-Construction Data Pipelines at Zero Cost

Pipeline Denotational Design (PDD) is a design-first methodology for building data pipelines that are correct by construction. As AI agents generate pipeline code at scale, the bottleneck shifts from writing to verifying pipelines, and the errors that matter most (grain inconsistencies that silently inflate aggregates) evade schema checks, type checks, and sampled tests. PDD designs pipelines in a semantic domain rather than in code: a design is composed from a typed algebra of operations (the Pipeline Design Algebra, one instantiation) in which every well-typed composition is grain-correct by construction. Resting on grain alone, the guarantee is universal: it holds for any grain-inferring operation set, over any engine. Correctness is established in three layers (grain, behavioral class, and domain) at design time, at zero cost, with no access to data: grain by a data-independent computation (CalcG), behavioral class by the type checker, and domain rules by a proof-carrying composition over operation contracts. A Pipeline Correctness theorem collapses the rest to a single input-boundary check: the only data-dependent residue is whether inputs meet the design's preconditions (data quality, not code correctness), which PDD emits as SQL/PySpark verification queries. Correctness by construction is a spectrum: the same design can be verified by runtime checks, the deployed type-level checker, or machine-checked proofs in Agda/Lean 4. This recasts the engineer's role: an agent instantiates a pre-verified pattern and ships a machine-checkable certificate; the human validates a compact specification and checks it. We realize the methodology in a production toolchain and set out an evaluation across pipeline patterns, behavioral classes, and data modelling paradigms. Because it rests on grain alone, the same design-time check extends to AI-generated queries over semantic layers and ontologies.

cs.DB↗

arXiv2026

Grain Theory: Type-Level Granularity Correctness in Data Pipelines

Data transformation correctness is a fundamental challenge in data engineering: how can we verify that pipelines produce correct results before executing on production data? Existing practice relies on iterative testing over materialized data. A common cause of errors is the absence of formal reasoning about grain -- the level of detail of data -- so transformations inadvertently change granularity, yielding pathologies like fan traps (metric duplication) and chasm traps (data loss). We introduce grain theory, a type-theoretic framework that elevates grain to a composable property of any algebraic data type. It has two phases. First, a denotation of data: grain itself, defined by irreducibility and isomorphism, with no reference to functional dependencies; three grain relations forming a bounded lattice whose axioms recover Armstrong's on product types; the entity key as a derived grain; and grain-determined behavioral classes -- together the type-level triple (G[R], EK[R], BC[R]). Second, a denotation of transformations: every transformation $h$ has a grain lift $φ(h)$. For collections of product types under the relational algebra we prove an equi-join grain inference theorem and present CalcG, a decidable algorithm that composes grain lifts across a pipeline DAG. The central theorem -- the grain homomorphism -- ties the phases together: grain projection commutes with transformation, and grain lifts compose ($φ(h_2 \circ h_1) = φ(h_2) \circ φ(h_1)$). Grain-correctness is therefore verifiable at design time, before any code or query runs. As corollaries, fan traps emerge as schema-detectable grain-relation violations; chasm traps localize to a specific ordering-chain pattern; and behavioral-class violations, such as point-in-time queries on the wrong collection type, become compile-time type errors. All theorems are mechanically verified in Lean 4.

cs.DB↗

arXiv2022

Babel Fees via Limited Liabilities

Custom currencies (ERC-20) on Ethereum are wildly popular, but they are second class to the primary currency Ether. Custom currencies are more complex and more expensive to handle than the primary currency as their accounting is not natively performed by the underlying ledger, but instead in user-defined contract code. Furthermore, and quite importantly, transaction fees can only be paid in Ether. In this paper, we focus on being able to pay transaction fees in custom currencies. We achieve this by way of a mechanism permitting short term liabilities to pay transaction fees in conjunction with offers of custom currencies to compensate for those liabilities. This enables block producers to accept custom currencies in exchange for settling liabilities of transactions that they process. We present formal ledger rules to handle liabilities together with the concept of babel fees to pay transaction fees in custom currencies. We also discuss how clients can determine what fees they have to pay, and we present a solution to the knapsack problem variant that block producers have to solve in the presence of babel fees to optimise their profits.

cs.CR↗