SHF: Small: Revisiting Elementary Denotational Semantics

SHF：小：重新审视基本指称语义

基本信息

批准号：
1814460
负责人：
Jeremy Siek
金额：
$ 38.07万
依托单位：
Indiana University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-10-01 至 2022-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1814460&HistoricalAwards=false
关键词：
SHF Small Revisiting Elementary Denotational

项目摘要

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.

编程语言理论和形式化方法的进步使研究人员能够指定完整的编程语言，验证其编译器的正确性，并证明特定程序是正确的。然而，就目前的技术水平而言，这样的证明是乏味的并且需要艰巨的工作。该项目的影响将是通过发现指定编程语言的新技术来极大地简化此类工作，这些技术可以更好地与证明的结构保持一致。该项目的新颖之处在于对指称语义的实际应用的调查，这些语义是基本的，基于集合论而不是领域理论。当今指定编程语言的首选方法是操作语义。这种语义在数学上很简单，并且与实现相距不远。然而，使用操作语义的正确性证明通常需要繁琐的模拟和句法逻辑关系。回顾 20 世纪 80 年代，研究人员更喜欢指称语义，它可以对程序片段进行组合推理。然而，大多数指称语义都涉及复杂的数学，这导致进展缓慢并为采用设置了障碍。这是大多数，但不是全部。 20 世纪 70 年代，Scott、Plotkin 和 Engeler 发明了 lambda 演算的图模型。 20 世纪 70 年代末，都灵小组发明了滤波器模型。这些所谓的基本模型结合了两全其美的优点：它们在数学上很简单，并且具有组合性，可以进行方程推理。不幸的是，由于历史上的一些意外，这些模型并没有流行起来，也从未应用于完整的编程语言或编译器正确性的证明。该项目将确定基本模型是否有利于语言规范、机械化元理论和编译器正确性的日常工作。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值进行评估，被认为值得支持以及更广泛的影响审查标准。