Dimensionally correct by construction: Type systems for programs
Event Information
About this event
SPEAKERS
Conor McBride
Fredrik Nordvall Forsberg
AGENDA
17:15 - Networking
18:00 - Speakers’ presentation
19:00 - Questions & discussion
19:15 - Networking
20:00 - Webinar ends
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.
SPEAKER BIOGRAPHIES
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:
Formal Aspects of Computing SG
https://www.bcs.org/membership/member-communities/facs-formal-aspects-of-computing-science-group/
Organiser BCS, The Chartered Institute for IT
Organiser of Dimensionally correct by construction: Type systems for programs
We are all responsible for ensuring technology-led change is safe and positive for everyone in society. At BCS we’re committed to meeting this responsibility under royal charter.
That’s why we set the highest standards of professionalism and best practice in the industry, share knowledge, and develop skills and capability tuned to our evolving digital world.
We’ve been supporting the technology industry since 1957 and our 73,000-strong membership spans 150 countries. Every member actively promotes IT professionalism and we provide them with career development opportunities and bring the community together to address the professional, ethical and economic challenges facing technology today.
