
A
Sound
Type
System
for
Physical
Quantities,
Units,
and
Measurements
Title: 
A Sound Type System for Physical Quantities, Units, and Measurements 
Authors:

Simon Foster and
Burkhart Wolff

Submission date: 
20201020 
Abstract: 
The present Isabelle theory builds a formal model for both the
International System of Quantities (ISQ) and the International System
of Units (SI), which are both fundamental for physics and engineering.
Both the ISQ and the SI are deeply integrated into Isabelle's
type system. Quantities are parameterised by dimension types, which
correspond to base vectors, and thus only quantities of the same
dimension can be equated. Since the underlying "algebra of
quantities" induces congruences on quantity and SI types,
specific tactic support is developed to capture these. Our
construction is validated by a testset of known equivalences between
both quantities and SI units. Moreover, the presented theory can be
used for typesafe conversions between the SI system and others, like
the British Imperial System (BIS). 
BibTeX: 
@article{Physical_QuantitiesAFP,
author = {Simon Foster and Burkhart Wolff},
title = {A Sound Type System for Physical Quantities, Units, and Measurements},
journal = {Archive of Formal Proofs},
month = oct,
year = 2020,
note = {\url{https://isaafp.org/entries/Physical_Quantities.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
