SHF: Small: Revisiting Elementary Denotational Semantics

编程语言理论和形式化方法的进步使研究人员能够指定完整的编程语言，验证其编译器的正确性，并证明特定程序是正确的。然而，在目前的技术水平下，这样的证明是乏味的，需要英勇的工作。该项目的影响将是通过发现新的技术来指定更符合校样结构的编程语言，从而极大地简化这类工作。该项目的新奇之处在于对基于集合论而不是领域理论的初级指称语义的实际应用进行了调查。目前，指定编程语言的首选方法是操作语义学。这样的语义在数学上很简单，而且离实现并不太远。然而，使用操作语义的正确性证明通常需要繁琐的模拟和句法逻辑关系。回顾20世纪80年代，研究人员更喜欢指称语义，它允许对程序片段进行组合推理。然而，大多数外延语义涉及复杂的数学，这导致进展缓慢，并为采用制造了障碍。大部分都是，但不是全部。在20世纪70年代，Scott、Plotkin和Engeler发明了Lambda微积分的图形模型。20世纪70年代末，都灵集团发明了过滤器模型。这些所谓的初级模型结合了两个世界的最好：它们在数学上很简单，而且它们是组合的，这使得等式推理成为可能。不幸的是，由于历史上的某种偶然，这些模型并没有流行起来，也从未被应用于完整的编程语言或编译器正确性的证明。该项目将确定初级模型是否适合语言规范、机械化元理论和编译器正确性的日常工作。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.