Type systems for programs respecting dimensions

McBride, Conor and Nordvall Forsberg, Fredrik; (2021) Type systems for programs respecting dimensions. In: Advanced Mathematical and Computational Tools in Metrology and Testing XII. Series on Advances in Mathematics for Applied Sciences . World Scientific Publishing Co. Pte Ltd, BIH. (In Press)

[thumbnail of McBride-etal-amctmtxii2021-type-systems-for-programs-respecting-dimensions]
Preview
 Text. Filename: McBride_etal_amctmtxii2021_type_systems_for_programs_respecting_dimensions.pdf
Accepted Author Manuscript
Download (332kB)| Preview

Abstract

Type systems can be used for tracking dimensional consistency of numerical computations: we present an extension from dimensions of scalar quantities to dimensions of vectors and matrices, making use of dependent types from programming language theory. We show that our types are unique, and most general. We further show that we can give straightforward dimensioned types to many common matrix operations such as addition, multiplication, determinants, traces, and fundamental row operations.

ORCID iDs

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