Approximate Normalization and Eager Equality Checking for Gradual Inductive Families

Joseph Eremondi, Ronald Garcia, Éric Tanter

Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In parti…