Spreadsheet verification and type systems have been studied extensively by the rather terrifyingly productive Martin Erwig. See http://web.engr.oregonstate.edu/

Spreadsheet verification and type systems have been studied extensively by the rather terrifyingly productive Martin Erwig. See http://web.engr.oregonstate.edu/~erwig/papers/abstracts.html http://web.engr.oregonstate.edu/~erwig/papers/abstracts.html, and scroll down the page. "Software Engineering for Spreadsheets" "Automatic Detection of Dimension Errors in Spreadsheets" "Type Inference for Spreadsheets" etc.