Dimensionally correct by construction: Type systems for programs respecting dimensions.
Watch the video
Synopsis
Physical dimensions such as length, mass and time can be used to ensure that equations are physically meaningful - it makes no sense to add 7 metres to 12 seconds. From a computer science perspective, there is a strong similarity between physical dimensions and types in programming languages, and indeed, Andrew Kennedy explored this connection in the 1990s. Modern type systems not only tell you off when you get things wrong, but also help you to get things right, e.g. by using types for code generation, or to guide the search for the correct program.
We show that they are also expressive enough to not only encode the physical dimensions of single scalars, but also of vectors and matrices, and to type basic linear algebra operations such as matrix multiplication and Gaussian elimination. Convincing our type checker that the pieces fit together properly required us to increase significantly the amount of algebra it is willing to do for itself, and in the process, we learned a lot.
About the speakers
The speakers are a Reader (Conor McBride) and Strathclyde Chancellor's Fellow (Fredrik Nordvall Forsberg) in the area of Computer and Information Sciences at the University of Strathclyde.
Our events are for adults aged 16 years and over.
This event is brought to you by: BCS FACS SG - Formal Aspects of Computing
