http://homepage.divms.uiowa.edu/~tinelli/papers/BraEtAl-ARITH-15.pdf

I have sent a link to a paper which tries to have formal semantics
for floating point numbers. We have shifted to manually specifying
types which should be matrix elements by using `is_matrix_element`
trait. However, I feel this would be instructive to look at anyway.

-- 
Best
Jayesh Badwaik
https://jayeshbadwaik.github.io