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

题目：SHF：小：SEQUBE：高级和中级编程语言的序列微积分基础现代编程语言是复杂的。它们提供了复杂的控制机制，提供了不同编程范式（例如，函数式或面向对象）的组合，并允许定义无限的对象和进程（例如，服务器或操作系统）。为了在我们的软件中获得保证，从根本上来说，重要的是要有一个简单而直观的框架来对使用这些特性的程序进行推理和实验：无论是对于编程语言的设计者和实现者，还是对于需要证明关键应用程序的安全属性的程序员。传统上，λ演算是编写和证明程序性质的基础。本研究的智力价值在于开发了一种基于顺序演算的替代程序模型。新模型没有从核心语言开始，并根据需要在上面分层功能，而是从一开始就自然地包含了这些功能。与λ演算一样，基于序列的模型起源于逻辑，但植根于对偶概念，该概念提供了两种解决问题的方法，其中一种通常更熟悉。此外，基于顺序的模型提供了一种新的方法来组织编译器中使用的中间语言，以帮助程序优化和分析。这项研究的更广泛影响包括为不同社区之间传播知识提供了一种工具。由于新模型自然地将函数式范式和面向对象范式作为双重性来包含，因此它提供了对语言（如Scala）的逻辑解释，将这两种方法合并在一起。此外，该研究将探索如何将无限过程的推理和计算效果结合在证明助手中。最后，强调二元性有利于教育；给定两种可能的解释，在介绍困难的概念时，可以先向学生介绍更熟悉的解释，同时利用现有的知识和直觉探索新的概念。

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.