University of Birmingham > Talks@bham > Theoretical computer science seminar > Some applications of free extensions to partial evaluation, equational-proof synthesis, and normalisation-by-evaluation

Some applications of free extensions to partial evaluation, equational-proof synthesis, and normalisation-by-evaluation

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact George Kaye.

Note unusual time because of interviews

Zoom details

The free extension (frex) offers a uniform theoretical foundation for the collection of partial-evaluation techniques known as partially-static data structures. The frex approach identifies concepts from universal algebra with concepts from partially-static data structures: signature with syntax; equations with semantics; algebra with static domain; and free extension with open-terms modulo semantics. This identification allows us to design and implement generic partial evaluators, with promising results regarding code-reuse and modularly.

I will start by motivating the use of algebra for partial evaluation from first principles, and introduce the concept of a free extension. Then I will review our existing and recent work applying this approach to staged partial evaluation and equational-proof synthesis in dependently-typed languages. Time-permitting, I will outline ongoing work. First, developing generic algorithms for normalisation-by-evaluation modulo algebraic-structure. Second, concerning the modular construction of free extensions.

Joint work with: Guillaume Allais, Edwin Brady, Greg Brown, Nathan Corbyn, Tamara von Glehn, Sam Lindley, Nachi Valliappan, and Jeremy Yallop.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.