- New pre-print on arXiv (and submitted to JFP):
- Title: “Types, equations, dimensions and the Pi theorem”
- Authors: N. Botta, P. Jansson, G. da Silva
- Blog post: http://patrikja.owlstown.net/posts/1796
- arXiv: https://arxiv.org/abs/2308.09481
- 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” ( https://patrikja.owlstown.net/posts/1385 ).
- Talk 2022-11-11 YouTube video
- at the Agda meeting in Edinburgh.
- Joint work with Nicola Botta and Guilherme Silva.
- Blog post
This talk describes work in progress aimed at understanding dimension analysis though coding it up using dependent types.
- This file loads in Agda 2.6.2.2 with Agda stdlib-1.7
- It is a literate Agda file with emacs org-mode syntax for outlining.