Work It, Wrap It, Fix It, Fold It

This page contains supplementary material for the article "Work It, Wrap It, Fix It, Fold It".

A mechanical verification of the proofs in Agda is available as a tarball, or it can be browsed below as hyperlinked HTML (recommended).

• CPO.agda — encoding of complete partial orders and continuous functions.

• FixTheorems.agda — useful theorems about complete partial orders.

• WWFix.agda — worker/wrapper transformation for least fixed points.

• FoldTheorems.agda — useful theorems about folds.

• FoldTheoremsInstantiated.agda — theorems about folds generated by instantiating the general categorical theory of initial algebras, where this differs from the above.

• WWFoldCommon.agda — some definitions common to all of the following worker/wrapper transformations for folds.

• WWFoldInstantiate.agda — worker/wrapper transformation for folds in CPO, by instantiating the general categorical theory.

• WWFoldDerived.agda — worker/wrapper transformation for folds in CPO, derived from the worker/wrapper transformation for least fixed points.

• WWFoldDirect.agda — worker/wrapper transformation for folds in CPO, proved from first principles.

Last updated 16th February 2016.