Type systems for programs respecting dimensions

Reference. Type systems for programs respecting dimensions

Conor McBride, Fredrik Nordvall Forsberg · Advanced Mathematical and Computational Tools in Metrology and Testing XII · 2022 · dimension-types · DOI

Cite

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

BibTeX

bibtex · 1 line

@inbook{mcbride-2022-type, title={Type systems for programs respecting dimensions}, ISSN={1793-0901}, url={http://dx.doi.org/10.1142/9789811242380_0020}, DOI={10.1142/9789811242380_0020}, booktitle={Advanced Mathematical and Computational Tools in Metrology and Testing XII}, publisher={WORLD SCIENTIFIC}, author={McBride, Conor and Nordvall-Forsberg, Fredrik}, year={2022}, month=Jan, pages={331–345} }

hayagriva YAML (typst)

yaml · 16 lines

mcbride-2022-type:
  type: chapter
  title: Type systems for programs respecting dimensions
  author:
  - McBride, Conor
  - Nordvall-Forsberg, Fredrik
  date: 2022-01
  page-range: 331-345
  url: http://dx.doi.org/10.1142/9789811242380_0020
  serial-number:
    doi: 10.1142/9789811242380_0020
    issn: 1793-0901
  parent:
    type: book
    title: Advanced Mathematical and Computational Tools in Metrology and Testing XII
    publisher: WORLD SCIENTIFIC

Download: mcbride-2022-type.bib · mcbride-2022-type.yml

Cited by (4)

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

Measuring with confidence: leveraging expressive type systems for correct-by-construction software mcbride-2023-measuringActa IMEKO · 2023

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.

DOI

EXPRESSIVE TYPE SYSTEMS FOR METROLOGY mcbride-2022-expressiveProceedings of the First International IMEKO TC6 Conference on Metrology and Digital Transformation - M4Dconf2022 · 2022

DOI

Cites 13 works (0 here)

External (13)

Pint: makes units easy (2020)
JSR 385: Units of measurement (2019)
A unit-aware matrix language and its application in control and auditing (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)
New equations for neutral terms: a sound and complete decision procedure, formalized (2013)
Boost C++ libraries, chapter 43 (Boost.Units 1.1.0) (2010)
Dependent Types at Work (2009)
Towards a practical programming language based on dependent type theory (2007)
The Mars Climate Orbiter Mishap Investigation Board Phase I Report (1999)
Programming languages and dimensions (1995)
Automatic dimensional inference (1991)