The simply-typed lambda calculus guarantees termination of programs, but termination is lost when adding unrestricted recursive types. One way to reconcile arbitrary self-references with termination is the use of a guarded typing discipline. We consider a guarded extension of the simply-typed lambda calculus, based on the work of Clouston et al. [2016], which features the so-called later type former ▸. The system admits unrestricted self-references (including negative ones), provided that a term of type τ refers to itself only ‘later’, at type ▸τ.

Executing such guarded programs efficiently is an open problem; at the same time, the ▸ type former and its associated term formers appear essential only to type checking, suggesting we can erase them while retaining the termination guarantee they provide. We present a program translation from the guarded language to untyped λ-calculus, for which we verify preservation of program behaviour, including termination. Our results are proved using a logical relation that interprets types in a step-indexed logic, and are machine-checked in the Rocq Prover using the Iris framework.

This is joint work with Bálint Kocsis and Robbert Krebbers.