Toward a Mechanized Compendium of Gradual Typing

Abstract

The research on gradual typing has grown considerably over the last decade, with more than 150 papers in the Gradual Typing Bibliography. There are a large number of alternative language designs that have been proposed and there are many interesting approaches for addressing the efficiency challenges. To better understand and categorize a central portion of the research on gradual typing, this article begins the development of a compendium of gradual typing, mechanized using the Agda proof assistant. This article identifies abstractions that capture similarities between many cast calculi, thereby enabling the reuse of definitions and theorems across different designs for many gradually typed languages.