Is anyone familiar with work that has been done on
unit composition in formal specifications within PVS? E.g.,
verifying that when you multiply meters by meters you get square
I have some ideas on what I want to do (and have
actually started down that path), but I don’t want to reinvent
the wheel if this has already been done.