POPL 2025 (series) / PEPM 2025 (series) / The 2025 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation /
A Fuelled Self-Reducer for System T (Short Paper)
This program is tentative and subject to change.
Self-reducers are programs that reduce embeddings of expressions to their normal forms. They are written in the same language that they reduce. To date, there are no self-reducers for strongly-normalising languages. I have implemented a fuelled self-reducer for System T. Rather than working with Gödel encodings, I used Kiselyov’s, and Longley and Normann’s encodings for structured types such as products, sums and some inductive types. Working with these types within System T produces large unreadable terms. I promote these structured types to first class features of a new metalanguage called Primrose. Primrose compiles into System T. Work on Primrose is ongoing.
Short paper (pepm25-paper1.pdf) | 155KiB |
This program is tentative and subject to change.
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
Tue 21 Jan
Displayed time zone: Mountain Time (US & Canada) change
14:00 - 15:30 | |||
14:00 45mKeynote | A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract) PEPM Brigitte Pientka McGill University | ||
14:45 30mResearch paper | Typed Program Analysis Without Encodings PEPM | ||
15:15 15mShort-paper | A Fuelled Self-Reducer for System T (Short Paper) PEPM Greg Brown University of Edinburgh File Attached |