Jacques: Created page with "A recurring task in program generation involves developing data-structures representing semantically-distinct code fragments. We can stage an optimised version of the original..."

2022-08-12T09:08:54Z

Created page with "A recurring task in program generation involves developing data-structures representing semantically-distinct code fragments. We can stage an optimised version of the original..."

New page

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.

WG211/M21Kammar - Revision history

Jacques: Created page with "A recurring task in program generation involves developing data-structures representing semantically-distinct code fragments. We can stage an optimised version of the original..."