  Logical relations are one of the most powerful techniques in the theory of
programming languages, and have been used extensively for proving properties of
a variety of higher-order calculi. However, there are properties that cannot be
immediately proved by means of logical relations, for instance program
continuity and differentiability in higher-order languages extended with
real-valued functions. Informally, the problem stems from the fact that these
properties are naturally expressed on terms of non-ground type (or,
equivalently, on open terms of base type), and there is no apparent good
definition for a base case (i.e. for closed terms of ground types). To overcome
this issue, we study a generalization of the concept of a logical relation,
called \emph{open logical relation}, and prove that it can be fruitfully
applied in several contexts in which the property of interest is about
expressions of first-order type. Our setting is a simply-typed
$\lambda$-calculus enriched with real numbers and real-valued first-order
functions from a given set, such as the one of continuous or differentiable
functions. We first prove a containment theorem stating that for any such a
collection of functions including projection functions and closed under
function composition, any well-typed term of first-order type denotes a
function belonging to that collection. Then, we show by way of open logical
relations the correctness of the core of a recently published algorithm for
forward automatic differentiation. Finally, we define a refinement-based type
system for local continuity in an extension of our calculus with conditionals,
and prove the soundness of the type system using open logical relations.
