Email Gateway (Oct 28 2020 at 11:29): Email Gateway (Oct 28 2020 at 11:29):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I happy to announce a new AFP entry.
Enjoy,
René
A Sound Type System for Physical Quantities, Units, and Measurements
by Simon Foster and Burkhart Wolff
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 test-set of known
equivalences between both quantities and SI units. Moreover, the presented
theory can be used for type-safe conversions between the SI system and others,
like the British Imperial System (BIS).
https://www.isa-afp.org/entries/Physical_Quantities.html
Last updated: Jul 15 2022 at 23:21 UTC