Logical Relations for Partial Features and Automatic Differentiation Correctness

Fernando Lucatelli Nunes, Matthijs Vákár

We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in catego…