A Fuelled Self-Reducer for System T (Short Paper)

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.