Compression Proofs

A compression algorithm attempts to reduce the size of a file of data by taking advantage of redundancy. Typically there are two function compress and decompress which act on a list of values - often bytes or characters. We consider a number of popular algorithms, we present an implementation in ML and a proof that the algorithm is correct, i.e. that decompress is the inverse of compress.