Coffee House talk: Ian Mackie on GoI-based compilation
▶ Very simple GOI for System T.
▶ Reversible machinery for higher-order language.
▶ Depending on how we constrain the use of the recursor, this language is rich enough to capture all primitive recursive functions or more generally Gödel’s System T.
▶ All implemented – benchmarks show that significant computations can be performed using very little run-time memory.
▶ Ongoing work: measure energy usage, program transformations.