![]() |
![]() |
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-evaluationAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsBritGrav 15 Analysis seminar Medical Imaging Research SeminarsOther talksQuantum Sensing in Space Ultrafast Spectroscopy and Microscopy as probes of Energy Materials Control variates for computing transport coefficients TBC Wave turbulence in the Schrödinger-Helmholtz equation TBA |