Type systems for programs respecting dimensions

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)peer-review

590 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationAdvanced Mathematical and Computational Tools in Metrology and Testing XII
Place of PublicationSingapore
PublisherWorld Scientific Publishing Co. Pte Ltd
Number of pages15
Publication statusAccepted/In press - 8 Jan 2021
EventAdvanced Mathematical and Computational Tools in Metrology and Testing XII - Sarajevo, Bosnia and Herzegovina
Duration: 15 Sept 202017 Sept 2020

Publication series

NameSeries on Advances in Mathematics for Applied Sciences
PublisherWorld Scientific
ISSN (Print)1793-0901

Conference

ConferenceAdvanced Mathematical and Computational Tools in Metrology and Testing XII
Abbreviated titleAMCTMT XII
Country/TerritoryBosnia and Herzegovina
CitySarajevo
Period15/09/2017/09/20

Keywords

  • units of measure
  • dimensions
  • type systems
  • dependent types

Fingerprint

Dive into the research topics of 'Type systems for programs respecting dimensions'. Together they form a unique fingerprint.

Cite this