Gradual Guarantee via Step-Indexed Logical Relations in Agda
Jeremy G. Siek
TL;DR
The paper presents the first mechanized proof of the gradual guarantee for the Gradually Typed Lambda Calculus using step-indexed logical relations implemented in Agda. It builds a Cast Calculus, defines a precision relation on types and terms, and develops a Step-Indexed Logic (SIL) to support a mutually recursive logical relation LRₜ⊎LRᵥ. Through a sequence of Compatibility Lemmas and a Fundamental Theorem, it shows that precision implies the logical relation, which then yields semantic approximation and ultimately the gradual guarantee. The work demonstrates the viability of a language-independent, mechanized metatheory approach via SIL and Abstract Binding Trees, and discusses practical trade-offs relative to simulation-based proofs. The methodology and libraries developed (ABT and SIL) provide reusable infrastructure for mechanizing similar proofs in Agda.
Abstract
The gradual guarantee is an important litmus test for gradually typed languages, that is, languages that enable a mixture of static and dynamic typing. The gradual guarantee states that changing the precision of a type annotation does not change the behavior of the program, except perhaps to trigger an error if the type annotation is incorrect. Siek et al. (2015) proved that the Gradually Typed Lambda Calculus (GTLC) satisfies the gradual guarantee using a simulation-based proof and mechanized their proof in Isabelle. In the following decade, researchers have proved the gradual guarantee for more sophisticated calculi, using step-indexed logical relations. However, given the complexity of that style of proof, there has not yet been a mechanized proof of the gradual guarantee using step-indexed logical relations. This paper reports on a mechanized proof of the gradual guarantee for the GTLC carried out in the Agda proof assistant.