### 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 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).

### License

BSD License

### Topics

- Mathematics/Physics
- Computer science/Programming languages/Type systems

### Session Physical_Quantities

- Power_int
- Enum_extra
- Groups_mult
- ISQ_Dimensions
- ISQ_Quantities
- ISQ_Proof
- ISQ_Algebra
- ISQ_Units
- ISQ_Conversion
- ISQ
- SI_Units
- CGS
- SI_Constants
- SI_Prefix
- SI_Derived
- SI_Accepted
- SI_Imperial
- SI
- SI_Astronomical
- SI_Pretty
- BIS

## Cite

×

Physical_Quantities-AFP

    @article{Physical_Quantities-AFP,
      author  = {Simon Foster and Burkhart Wolff},
      title   = {A Sound Type System for Physical Quantities, Units, and Measurements},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Physical_Quantities.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Oct 28, 2020 : Isabelle2020