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

Tools

McBride, Conor and Nakov, Georgi and Nordvall Forsberg, Fredrik (2023) Measuring with confidence : leveraging expressive type systems for correct-by-construction software. Acta IMEKO, 12 (1). 15. ISSN 2221-870X (https://doi.org/10.21014/actaimeko.v12i1.1412)

[thumbnail of McBride-etal-AI-2023-Measuring-with-confidence-leveraging-expressive-type]
Preview
 Text. Filename: McBride_etal_AI_2023_Measuring_with_confidence_leveraging_expressive_type.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (608kB)| Preview

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.

ORCID iDs

McBride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886, Nakov, Georgi and Nordvall Forsberg, Fredrik ORCID logoORCID: https://orcid.org/0000-0001-6157-9288;
CORE (COnnecting REpositories)