SHF: Small: Revisiting Elementary Denotational Semantics

程序设计语言理论和形式化方法的进步使研究人员能够指定完整的程序设计语言，验证其编译器的正确性，并证明特定程序是正确的。然而，以目前的技术水平，这样的证明是乏味的，需要英勇的工作。该项目的影响将是通过发现与证明结构更好地一致的指定编程语言的新技术，从而大大简化此类工作。这个项目的新颖之处在于对基于集合论而非领域论的基本指称语义的实际应用的研究。目前指定编程语言的首选方法是操作语义。这样的语义在数学上很简单，而且离实现也不远。然而，使用操作语义的正确性证明通常需要精细的模拟和语法逻辑关系。回顾20世纪80年代，研究人员更倾向于指称语义，它可以对程序片段进行组合推理。然而，大多数指称语义学涉及复杂的数学，这使得进展缓慢，并为采用创造了障碍。大部分是这样，但不是全部。在20世纪70年代，Scott， Plotkin和Engeler发明了lambda微积分的图形模型。在20世纪70年代末，都灵小组发明了过滤器模型。这些所谓的基本模型结合了两个世界的优点：它们在数学上是简单的，它们是组合的，这使得方程推理成为可能。不幸的是，由于历史上的一些偶然事件，这些模型并没有流行起来，也从未应用于完整的编程语言或编译器正确性的证明。该项目将确定基本模型是否适合语言规范、机械化元理论和编译器正确性的日常工作。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.