← 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 · v2 cs.LO
All theorems of the units-of-measure calculus (abstraction, adequacy, erasure, Pi theorem) are mechanized in Lean 4, with an evaluator compiled to a native binary.
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 guarantee that well-typed programs are invariant under rescaling of units, but they exclude unit conversion. Practical languages allow conversion but offer no invariance theorem. The open question is how much invariance survives once conversion is added.

The authors define Λ_S, a typed lambda calculus with unit conversion, quantification over units and dimensions, and vectors and linear maps with per-component units. Units are rational exponent vectors related to dimensions by a homomorphism, and conversion factors are given by valuations. Unit abstractions denote families of meanings indexed by magnitudes. Abstraction theorems are proved with logical relations. They also build a drift-based decision procedure for first-order programs, a declaration consistency checker, and a fuel-based evaluator, all in Lean 4.

Convert-free parametric terms are invariant under every rescaling, and terms with conversions are invariant exactly under coherent (per-dimension) rescalings. The development includes a verified three-verdict drift diagnostic, a verified declaration checker with exact factor extraction, adequacy, erasure, square-root non-definability, and the n-variable Pi theorem. Everything is mechanized in Lean 4.