A Fuelled Self-Reducer for System T - Short Paper

Explore a short conference talk by Greg Brown from the University of Edinburgh presenting his implementation of a fuelled self-reducer for System T, a strongly-normalising language. Learn how this innovative approach uses Kiselyov's and Longley and Normann's encodings for structured types instead of Gödel encodings, and discover the development of Primrose, a new metalanguage that promotes structured types to first-class features while compiling into System T. This 15-minute presentation from the PEPM 2025 conference (sponsored by ACM SIGPLAN) offers insight into ongoing work that addresses the challenge of creating self-reducers for strongly-normalising languages.