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

• Ohad Kammar (University of Edinburgh)
• Friday 24 March 2023, 11:00-11:50
• LG23, Computer Science // Zoom.

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

Note unusual time because of interviews

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09
• Meeting ID: 818 7333 5084
• Passcode: 217

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.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, Computer Science // Zoom
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.