SHF: Small: SEQUBE: A Sequent Calculus Foundation for High- Level and Intermediate Programming Languages

SHF：小型：SEQUBE：高级和中级编程语言的顺序微积分基础

• 批准号: 1423617
• 负责人: Zena Ariola
• 金额: $ 50万
• 依托单位: University of Oregon Eugene
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-07-01 至 2019-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1423617&HistoricalAwards=false
• 关键词: SHF; Small; SEQUBE; Sequent; Calculus

Title: SHF:Small:SEQUBE:A Sequent Calculus Foundation for High-Level and Intermediate Programming LanguagesModern programming languages are complex. They provide sophisticated control mechanisms, offer a combination of different programming paradigms (e.g., functional or object-oriented), and allow the definition of infinite objects and processes (e.g., servers or operating systems). To have assurance in our software, it is fundamentally important to have a simple and intuitive framework for reasoning about and experimenting with programs that use these features: both for programming language designers and implementors, as well as for programmers who need to prove safety properties of critical applications.Traditionally, the lambda-calculus has served as a foundation for writing and proving properties of programs. The intellectual merit of this research consists of developing an alternative model of programs based on the sequent calculus. Instead of starting from a core language and layering features on top as needed, the new model naturally includes these features from the beginning. Like the lambda-calculus, the sequent-based model originates from logic, but is rooted in the concept of duality that provides two ways to approach problems, where one is often more familiar. Additionally, the sequent-based model provides a new way to organize intermediate languages used in compilers to aid program optimization and analysis.The broader impact of the research consists of providing a vehicle for disseminating knowledge between different communities. Since the new model includes both the functional and object-oriented paradigms naturally as duals, it provides a logical interpretation of languages, such as Scala, that merge the two approaches. In addition, the research will explore ways to incorporate reasoning about infinite processes and computational effects in a proof assistant. Lastly, an emphasis on duality is beneficial for education; given two possible explanations, students can be introduced to the more familiar one first when introducing difficult ideas, while using existing knowledge and intuition to explore new concepts.

标题：SHF：SMALL：SECEBE：高级和中级编程语言的序列计算基础很复杂。它们提供了复杂的控制机制，提供了不同编程范式（例如功能或面向对象）的组合，并允许定义无限的对象和过程（例如服务器或操作系统）。 为了保证我们的软件，拥有一个简单，直观的框架来推理和实验使用这些功能的程序：用于编程语言设计师和实施者以及需要证明关键应用程序安全性的程序员的程序。这项研究的智力优点包括开发基于序列的替代程序模型。 新模型从一开始就自然包含了这些功能，而不是从需要的核心语言和上层功能开始。像lambda-calculus一样，基于序列的模型源自逻辑，但植根于双重性的概念，提供了两种方法来解决问题的方法，在这些方法中通常更熟悉。此外，基于序列的模型还提供了一种新的方法来组织编译器中使用的中间语言，以帮助计划优化和分析。研究的更广泛影响包括提供一种用于在不同社区之间传播知识的工具。由于新模型自然地包括功能性和面向对象的范例，因此它提供了对语言（例如Scala）的逻辑解释，例如Scala，可以合并两种方法。此外，该研究将探讨将有关无限过程和计算效应的推理纳入证明助手的方法。最后，对二元性的重视对教育有益。给定两个可能的解释，可以在介绍困难的想法时首先将学生介绍给更熟悉的一个，同时使用现有知识和直觉来探索新概念。