Title: Revisiting Elementary Denotational Semantics,
Abstract: Operational semantics have been enormously successful, in large part due to
its flexibility and simplicity, but they are not compositional. Denotational
semantics, on the other hand, are compositional but the lattice-theoretic
models are complex and difficult to scale to large languages. However, there
are elementary models of the $\lambda$-calculus that are much less complex: by
Coppo, Dezani-Ciancaglini, and Salle (1979), Engeler (1981), and Plotkin
(1993).
This paper takes first steps toward answering the question: can elementary
models be good for the day-to-day work of language specification,
mechanization, and compiler correctness? The elementary models in the
literature are simple, but they are not as intuitive as they could be. To
remedy this, we create a new model that represents functions literally as
finite graphs. Regarding mechanization, we give the first machine-checked proof
of soundness and completeness of an elementary model with respect to an
operational semantics. Regarding compiler correctness, we define a polyvariant
inliner for the call-by-value $\lambda$-calculus and prove that its output is
contextually equivalent to its input. Toward scaling elementary models to
larger languages, we formulate our semantics in a monadic style, give a
semantics for System F with general recursion, and mechanize the proof of type
soundness.