权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。