hazel

This paper introduces a theory of bidirectional type slicing, where selecting a term and querying its type information yields a minimal program slice sufficient to explain that type. The metatheory is mechanised in Agda and a linear-time approximation is implemented for the Hazel programming environment.