课题基金 / 基金详情

SHF: SMALL: Semantically and Practically Generalizing Graded Modal Types

SHF: SMALL: Semantically and Practically Generalizing Graded Modal Types
SHF:SMALL:语义和实践上概括分级模态类型
批准号:
2104535
负责人:
Harley Eades
金额:
$42.64万
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2021
资助国家:
美国
项目状态:
未结题
起止时间:
2021-04-15 至 2025-03-31

项目摘要

项目成果

Harley Eades的其他基金

相似基金

相关文献

中文摘要
翻译
在过去三十年的过程中,研究编程语言的计算机科学家致力于两个主要问题:如何将软件验证合并到典型的软件开发人员的工作流程中,以及如何扩展软件验证以支持对数据使用的推理,例如,防止滥用内存和套接字句柄。这个项目的主要新颖之处在于纠正数据滥用的问题:该研究概括并结合了用于数据使用推理的程序逻辑,以及现代编程语言中使用的验证工具的功能,在单一实用的通用编程语言中。该项目的优点是:(1)发展了一种新的一般理论,其他人可以用来研究和采用这种新的组合;(2)一种新的编程语言Tenli,它包含了这种新的强大组合;(3)为本科和研究生阶段的教学资源软件验证设计新的教材。这项工作的一个主要的更广泛的影响是在这个项目中纳入了广泛的学生,例如,来自佐治亚州研究型大学奥古斯塔大学的本科生,佐治亚州历史悠久的文理女子学院卫斯理学院,佐治亚州历史悠久的私立卫理公会黑人大学克拉克亚特兰大,以及奥古斯塔大学的第一批研究生。该项目结合了两种强大的验证方法:(1)基于类型的验证,以及(2)通过分级模态类型跟踪数据使用情况。分级模态类型被推广到支持对广泛的数据使用跟踪的推理,包括对命令式数据结构的推理。基于伴随逻辑的概念,提出了一种新的梯度模态类型理论,并在此基础上开发了一种新的实用的通用依赖类型编程语言Tenli。此外,正在Tenli内部进行几个案例研究,以评估其实用性。该奖项反映了美国国家科学基金会的法定使命,并通过使用基金会的知识价值和更广泛的影响审查标准进行评估,被认为值得支持。
英文摘要
Over the course of the last thirty years, computer scientists studying programming languages have worked on two major problems: how to incorporate software verification into the typical software developer's work flow, and how to extend software verification to support reasoning about data usage, for example, preventing the misuse of memory and socket handles. The main novelties of this project are to rectify this problem of misuse of data: the research generalizes and combines program logics for reasoning about data-usage, and the power of verification tools used in modern programming languages, within a single practical general-purpose programming language. The project's merits are: (1) The development of a new general theory that others can use to study and adopt this new combination; (2) A new programming language, Tenli, that encompasses this new powerful combination; and (3) The design of new pedagogical materials for teaching resourceful software verification at both the undergraduate and graduate levels. A major broader impact of this work is the incorporation of a wide range of students in this project, e.g., undergraduate students from Augusta University, a research university in Georgia, Wesleyan College, a historical liberal arts women's college in Georgia, and Clark Atlanta, a private Methodist historically black university in Georgia, and the first cohort of graduate students at Augusta University.This project combines two powerful verification methodologies: (1) type-based verification, and (2) data-usage tracking through graded modal types. Graded modal types are generalized to support reasoning about a wide range of data-usage tracking including reasoning about imperative data structures. Both a new theory of graded modal types based on the notion of adjoint logics and a new practical general-purpose dependently-typed programming language, Tenli, are developed based on this new theory. Furthermore, several case studies within Tenli are being conducted to gauge its practicality.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.
期刊论文(1)
专著(0)
科研奖励(0)
会议论文
A Dependent Dependency Calculus
依赖依赖演算
DOI: 10.1007/978-3-030-99336-8_15
发表时间: 2022
期刊: Lecture notes in computer science
影响因子: --
作者: [Choudhury, Pritam, Eades III, Harley, Weirich, Stephanie]
通讯作者: Weirich, Stephanie
NSF Student Travel Grant for 2019 Southeast Regional Programming Languages Seminar (SERPL)
CRII: SHF: A New Foundation for Attack Trees Based on Monoidal Categories
国内基金
海外基金
昼夜节律性small RNA在血斑形成时间推断中的法医学应用研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    --
  • 批准年份:
    2024
  • 负责人:
  • 依托单位:
tRNA-derived small RNA上调YBX1/CCL5通路参与硼替佐米诱导慢性疼痛的机制研究
  • 批准号:
  • 项目类别:
    省市级项目
  • 资助金额:
    10.0万元
  • 批准年份:
    2022
  • 负责人:
    张祥忠
  • 依托单位:
Small RNA调控I-F型CRISPR-Cas适应性免疫性的应答及分子机制
Small RNAs调控解淀粉芽胞杆菌FZB42生防功能的机制研究
  • 批准号:
    31972324
  • 项目类别:
    面上项目
  • 资助金额:
    58.0万元
  • 批准年份:
    2019
  • 负责人:
    高学文
  • 依托单位: