Equational Reasoning in Fine Grain Algorithms

Dr John O'Donnell, University of Glasgow

Algorithms expressed using a small collection of combinators, including map, fold, scan, and sweep, can be implemented efficiently on circuits, FPGAs, and GPGPUs. Equational reasoning is effective for deriving such algorithms and proving them correct. I will describe its use in recent and current work on a family of algorithms related to functional arrays.