Measuring with confidence: leveraging expressive type systems for correct-by-construction software

Reference. Measuring with confidence: leveraging expressive type systems for correct-by-construction software

Conor McBride, Georgi Nakov, Fredrik Nordvall Forsberg · Acta IMEKO · 2023 · dimension-types · DOI

Modern programming language type systems help programmers write correct software, and furthermore helps them write the software they actually intended to write. We show how expressive types can be used to encode dimension and units of measure information, which can be used to avoid dimensional mistakes and guide software construction, and how types can even help to generate code automatically, which eliminates a whole class of bugs.

Cite

Cite as @mcbride-2023-measuring (helia, typst) · \cite{mcbride-2023-measuring} (LaTeX)

BibTeX

bibtex · 1 line

@article{mcbride-2023-measuring, title={Measuring with confidence: leveraging expressive type systems for correct-by-construction software}, volume={12}, ISSN={0237-028X}, url={http://dx.doi.org/10.21014/actaimeko.v12i1.1412}, DOI={10.21014/actaimeko.v12i1.1412}, number={1}, journal={Acta IMEKO}, publisher={IMEKO International Measurement Confederation}, author={McBride, Conor and Nakov, Georgi and Nordvall Forsberg, Fredrik}, year={2023}, month=Mar, pages={1–5} }

hayagriva YAML (typst)

yaml · 19 lines

mcbride-2023-measuring:
  type: article
  title: 'Measuring with confidence: leveraging expressive type systems for correct-by-construction software'
  author:
  - McBride, Conor
  - Nakov, Georgi
  - Nordvall Forsberg, Fredrik
  date: 2023-03
  page-range: 1-5
  url: http://dx.doi.org/10.21014/actaimeko.v12i1.1412
  serial-number:
    doi: 10.21014/actaimeko.v12i1.1412
    issn: 0237-028X
  parent:
    type: periodical
    title: Acta IMEKO
    publisher: IMEKO International Measurement Confederation
    issue: 1
    volume: 12

Download: mcbride-2023-measuring.bib · mcbride-2023-measuring.yml

Cited by (2)

Preserving model structure and constraints in scientific computing forbes-2025-preservingMeasurement: Sensors · 2025

DOI

LabMate: A prospectus for types for MATLAB mcbride-2025-labmateMeasurement: Sensors · 2025

DOI

Cites 19 works (1 here)

With notes (1)

Type systems for programs respecting dimensions mcbride-2022-typeAdvanced Mathematical and Computational Tools in Metrology and Testing XII · 2022

DOI

External (18)

Representing quantities and units in digital systems (2022)
Pint: makes units easy (2022)
MATLAB units of measurement (2022)
Software representation of measured physical quantities (2022)
JSR 385: units of measurement (2021)
Software for calculation with physical quantities (2020)
The International System of Units (SI Brochure), ninth edition (2019)
The next 700 unit of measurement checkers (2018)
A typechecker plugin for units of measure: domain-specific constraint solving in GHC Haskell (2015)
Experience report: type-checking polymorphic units for astrophysics research in Haskell (2014)
Quantities, units and computing (2013)
Type inference, Haskell and dependent types (2013)
Boost C++ libraries, chapter 42 (Boost.Units 1.1.0) (2010)
Dependent Types at Work (2009)
Types for Units-of-Measure: Theory and Practice (2009)
Programming languages and dimensions (1995)
Computation with finitely presented groups (1994)
Automatic dimensional inference (1991)