![]() |
![]() |
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 listsAnalysis seminar computer sience Metamaterials Research Group SeminarsOther talksSylow branching coefficients for symmetric groups Geometry of alternating projections in metric spaces with bounded curvature Modelling uncertainty in image analysis. TBC Extending the Lax type operator for finite W-algebras Quantum simulations using ultra cold ytterbium |