Patrik Jansson

Professor of Computer Science


Computer Science and Engineering

Chalmers University of Technology

Types, equations, dimensions and the Pi theorem

August 21, 2023

Last week we submitted a paper to JFP about dimension analysis in a (dependently) typed functional language (like Idris or Agda). It is also available (as a pre-print) on arXiv.

arXiv: 2308.09481
Authors: N. Botta, P. Jansson, G. da Silva
Abstract: The languages of mathematical physics and modelling are endowed with a rich “grammar of dimensions” that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to explain basic notions of dimensional analysis and Buckingham’s Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modelers and physicists.

I have talked about some aspects of the work earlier, and written about it in the post "Dimension analysis and graded algebras".


Follow this website

You need to create an Owlstown account to follow this website.

Sign up

Already an Owlstown member?

Log in