2022/01/13 by Conor McBride, Fredrik Nordvall Forsberg · 1 citation
Computer Science · #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Distributed and Parallel Computing Systems
paper · doi:10.1142/9789811242380_0020
openalex publication_date 2022/01/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/22
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.