Generic Programming with Extensible Data Types; Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
We provide an intrinsically-typed mechanization of System Rω with a shallow embedding / denotation into Agda. A suitable reviewer should have some experience with Agda, the Agda standard library, and language mechanization. The mechanization is a shallow embedding, so the metatheory follows from a total denotation. This means the artifact has very few of the lemmas, theorems, and infrastructure one might find in the mechanization of an operational semantics. However, by nature of embedding into a predicative system, our ASTs and denotational functions are burdened fairly heavily by level stratification. More experience with Agda over strict mechanization is thus welcome.