[TYPES] "Type systems for programs respecting dimensions" Re: Types for Units-of-Measure
Rodney Brown
rdbrown0au at gmail.com
Sat Apr 23 03:57:33 EDT 2022
For people who are interested :-
McBride, Conor; Nordvall-Forsberg, Fredrik (2022). "Type systems for
programs respecting dimensions" (PDF). Advanced Mathematical and
Computational Tools in Metrology and Testing XII. Advances in
Mathematics for Applied Sciences. World Scientific. pp. 331–345.
doi:10.1142/9789811242380_0020. ISBN 9789811242380.
https://urldefense.com/v3/__https://pureportal.strath.ac.uk/files/121022760/McBride_etal_amctmtxii2021_type_systems_for_programs_respecting_dimensions.pdf__;!!IBzWLUs!UX9RGwE5FC7pDxN47lDwNSXSAGRQyL5BgEzF1Jh82ctFk29TRks-axesIRwfnSzjWQsnkE7KCbhahp8xI9WTIixy-7kG5YI$
From the Conclusion:
Following Hart, we have shown how to use dependent types to extend type
systems for units of measure from scalars to matrices. ...
On 9/11/20 22:42, Rodney Brown wrote:
> Reading ACM SigPlan Notices in the 80s, the papers on adding
> Units-of-Measure to programming
> languages for type-checking seemed sensible - especially after reading
> Comp.risks in
> Software Engineering Notes.
>
> More recently I read George Hart's 1995 book "Multidimensional
> Analysis: ..." which provided
> the abstract algebra behind my vague intuitive understanding of
> Dimensional correctness,
> sketched an implementation and described the suprising (to me) result
> that some problems in
> science and engineering need matrices that aren't simply dimensionally
> uniform.
More information about the Types-list
mailing list