← All papers
First page of A Calculus for Units of Measure with Conversion

A Calculus for Units of Measure with Conversion

Eric Allen

cs.PL Sep 29, 2026 · v1 cs.LO
All theorems of the units-of-measure calculus (abstraction theorems, adequacy, erasure, Pi theorem, decision procedures) are mechanized in Lean 4; the evaluator compiles natively.
Programs that compute with physical quantities often need to convert between units of measurement, and as the Mars Climate Orbiter showed, these conversions can be a rich source of errors. Meanwhile, typed unit calculi, our most rigorous formalisms for checking physical units in a program, have excluded unit conversions. Through this exclusion, they have established a powerful property: well-typed programs are invariant under rescaling (no program can depend on how big a meter is). But losing the ability to convert between units is a significant cost. In contrast, practical languages provide conversion but no invariance theorem. We present $Λ_S$, a typed lambda calculus with conversion, quantification over units and dimensions, and vectors and linear maps with per-component units, and we determine exactly how much invariance survives conversion. For terms without unit constants we prove two abstraction theorems: (i) a convert-free term is invariant under every rescaling; (ii) a term with conversions is invariant under every rescaling that scales all units of one dimension by the same factor. The condition in (ii) cannot be weakened: under any other rescaling, some conversion of a nonzero value is not invariant. For first-order programs, a verified decision procedure returns one of three verdicts: it certifies that no error in the declared conversion factors can change the program's answer, names the accumulated ratio through which such an error would scale it, or declines. A verified checker decides whether unit declarations are consistent and determine every conversion factor, and extracts each factor exactly. We also prove adequacy, erasure, and the $n$-variable Pi theorem of dimensional analysis with conversion. Every theorem is mechanized in Lean 4, and the evaluator compiles to a native binary.

Typed unit calculi prove that well-typed programs are invariant under rescaling, but they exclude unit conversion. Practical languages allow conversion but provide no invariance guarantee. It has been unclear how much invariance survives once conversion is added.

The authors define Λ_S, a typed lambda calculus with unit conversion, quantification over units and dimensions, rational exponent vectors, and vectors and linear maps with per-component units. Semantics interpret unit abstraction as a family indexed by valuations, and logical relations are used to prove abstraction theorems. They build a verified drift-analysis decision procedure, a declaration-consistency checker with factor extraction, and a fuel-based evaluator. Everything is mechanized in Lean 4.

Convert-free terms are invariant under every rescaling, and terms with conversions are invariant exactly under dimension-coherent rescalings; this condition is shown to be tight. The paper also proves adequacy, erasure, non-definability of square root, and the n-variable Pi theorem with conversion. The evaluator compiles to a native binary.