Gradual Guarantee via Step-Indexed Logical Relations in Agda

TL;DR

This paper presents a mechanized proof of the gradual guarantee for the Gradually Typed Lambda Calculus (GTLC) using step-indexed logical relations in Agda, advancing formal verification in gradually typed languages.

Contribution

It provides the first mechanized proof of the gradual guarantee for GTLC with step-indexed logical relations in Agda, demonstrating the proof's formal correctness.

Findings

Mechanized proof of the gradual guarantee in Agda

Use of step-indexed logical relations for complex calculi

Advancement in formal verification of gradually typed languages

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.