David Läwen

Systems based on the Curry-Howard correspondence are rendered unsound by diverging terms; as such, self-referential definitions are typically restricted to ensure termination. For coinductive types, this involves checking productivity, i.e., that any finite prefix of the data can be computed in finite time. Syntactic conditions (such as Rocq’s productivity checker) can be used, but are known to reject valid productive definitions.

A more flexible approach due to Nakano [2000] is to enforce productivity through 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 definition of type τ refers to itself only ‘later’, at type ▸ τ.

Executing these 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 that we can erase them while retaining the strong guarantees they provide.

We present a program translation from the guarded language to untyped λ-calculus, for which we verify preservation of program behaviour, including productivity. To show that our source language enforces productivity, we give a mechanised proof of strong normalisation, an existing result from the literature. Both results are proved using a logical relation that interprets types in a step-indexed logic, and are machine-checked using the Rocq Prover and Iris framework.