Revisiting Elementary Denotational Semantics

TL;DR

This paper explores the potential of simple, elementary denotational models for practical language work, introducing a new graph-based model, mechanized proofs, and extending to System F with recursion.

Contribution

It introduces a new, more intuitive elementary denotational model, provides the first mechanized proofs of soundness and completeness, and extends the approach to larger languages like System F.

Findings

A new graph-based elementary model of the λ-calculus.

First machine-checked proof of soundness and completeness.

Extension of semantics to System F with recursion and proof of type soundness.

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.