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

Conor McBride; Georgi Nakov; Fredrik Nordvall Forsberg

doi:10.21014/actaimeko.v12i1.1412

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

Conor McBride, Georgi Nakov, Fredrik Nordvall Forsberg

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

50 Downloads (Pure)

Abstract

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.

Original language	English
Article number	15
Number of pages	5
Journal	Acta IMEKO
Volume	12
Issue number	1
DOIs	https://doi.org/10.21014/actaimeko.v12i1.1412
Publication status	Published - 22 Mar 2023

Keywords

metrology
programming languages
type systems
correctness

Access to Document

10.21014/actaimeko.v12i1.1412Licence: CC BY 4.0

McBride-etal-AI-2023-Measuring-with-confidence-leveraging-expressive-typeFinal published version, 594 KBLicence: CC BY 4.0

Trusted Systems
Ghani, N., McBride, C. & Nordvall Forsberg, F.
National Physical Laboratory NPL
1/10/19 → 30/09/24
Project: Research

Cite this

@article{acd5e654dc2d42f587f3c785fb2fd592,

title = "Measuring with confidence: leveraging expressive type systems for correct-by-construction software",

abstract = "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.",

keywords = "metrology, programming languages, type systems, correctness",

author = "Conor McBride and Georgi Nakov and {Nordvall Forsberg}, Fredrik",

year = "2023",

month = mar,

day = "22",

doi = "10.21014/actaimeko.v12i1.1412",

language = "English",

volume = "12",

journal = "Acta IMEKO",

issn = "2221-870X",

number = "1",

}

TY - JOUR

T1 - Measuring with confidence

T2 - leveraging expressive type systems for correct-by-construction software

AU - McBride, Conor

AU - Nakov, Georgi

AU - Nordvall Forsberg, Fredrik

PY - 2023/3/22

Y1 - 2023/3/22

N2 - 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.

AB - 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.

KW - metrology

KW - programming languages

KW - type systems

KW - correctness

U2 - 10.21014/actaimeko.v12i1.1412

DO - 10.21014/actaimeko.v12i1.1412

M3 - Article

SN - 2221-870X

VL - 12

JO - Acta IMEKO

JF - Acta IMEKO

IS - 1

M1 - 15

ER -

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

Abstract

Keywords

Access to Document

Fingerprint

Projects

Trusted Systems

Cite this