SHF: Small: Revisiting Elementary Denotational Semantics

Indiana University, Bloomington IN

Investigators

Abstract

Advances in programming language theory and formal methods have enabled researchers to specify complete programming languages, verify the correctness of their compilers, and prove that particular programs are correct. However, with the current state of the art, such proofs are tedious and require heroic work. The project's impact will be to greatly simplify such work by discovering new techniques for specifying programming languages that better align with the structure of the proofs. The project's novelty is in the investigation of practical applications of denotational semantics that are elementary, based on set theory rather than domain theory. The preferred approach today for specifying programming languages is operational semantics. Such semantics are mathematically simple and not too far removed from implementations. However, correctness proofs using operational semantics often require fiddly simulations and syntactic logical relations. Looking back to the 1980s, researchers preferred denotational semantics, which enable compositional reasoning about program fragments. However, most denotational semantics involved sophisticated mathematics, which made for slow progress and created barriers to adoption. Most that is, but not all. In the 1970s, Scott, Plotkin, and Engeler invented graph models of the lambda calculus. In the late 1970s, the Torino group invented filter models. These so-called elementary models combine the best of both worlds: they are simple mathematically and they are compositional, which enables equational reasoning. Unfortunately, by some accident of history, these models did not become popular and were never applied to complete programming languages or proofs of compiler correctness. The project will determine whether elementary models are good for the day-to-day work of language specification, mechanized meta-theory, and compiler correctness. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.