WG211/M21Kammar

A recurring task in program generation involves developing data-structures representing semantically-distinct code fragments. We can stage an optimised version of the original program off of its representation, taking advantage of semantic equivalences in the processs. Moreover, we may want to extract the detailed steps in the equational proof that the representation is equivalent to its source. These representations are known as partially-static data structures and semantic normal-forms. In recent and ongoing work, we specify these data structures using universal algebraic concepts, the free algebra and, its less familiar sibling, the free extension.

In this talk, I'll review our application of free extensions to staged-optimisation and proof-synthesis. Depending on audience participation, I'll either delve further into applications, give a tutorial on designing data structures based on free extensions, or sketch future directions.