Sparse matrix formats are typically implemented with low-level imperative 
programs.  The optimized nature of these implementations hides the structural 
organization of the sparse format and complicates its verification.
We formalize a proof system based on parametric predicates for tracking relationship 
between mathematical vectors and their concrete representations.  This proof 
theory automatically verifies full functional correctness of many formats.

This document contains the theories described in 

  Specifying and verifying sparse matrix codes
  by Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík,and Mooly Sagiv
  Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICP 2010)
  Pages 249 to 260 (doi: 10.1145/1863543.1863581)

This formalization works with Isabelle 2015.