POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Tue 21 Jan 2025 15:15 - 15:30 at Room 6 - Types and meta theory Chair(s): Kenichi Asai

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 Jan

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:30
Types and meta theoryPEPM at Room 6
Chair(s): Kenichi Asai Ochanomizu University
14:00
45m
Keynote
A Type-Theoretic Framework for Certified Meta-programming (Invited Talk Extended Abstract)
PEPM
Brigitte Pientka McGill University
14:45
30m
Research paper
Typed Program Analysis Without Encodings
PEPM
15:15
15m
Short-paper
A Fuelled Self-Reducer for System T (Short Paper)
PEPM
Greg Brown University of Edinburgh
File Attached