Research Initiation: Semantics and Logics of Programs

程序语义学最基本的目的是给出一个严格的， 明确定义程序的含义，提供一个 标准的翻译作者和用户的语言。 超出 这个基本目的、等式等关系放在程序片断上 可以被定义，导致逻辑推理程序， 程序转换的正式理由。 在过去 二十五年来，我们取得了巨大的进步。 最 重要的一步是语义领域的发展， 外延模型程序，这已经被扩展到模型 现代语言的结构，如赋值、分支和 非决定论 用于对程序进行推理的逻辑也被 为简单语言定义，使用语义域作为模型， 保证稳健。 困难在于如何扩大这些想法， 具有许多功能的成熟语言。 操作语义 这里提供了指称语义的替代方案，因为 总是在最底层的一个解释者，把脚放在 地面，并保持数学可管理。 这个项目需要一个 语义学的操作方法，目的是给语义 成熟的编程语言，并进一步定义丰富的 程序等价的概念，因此逻辑可以被定义。 因此，这项工作是许多不同种类的 语言语义学

The most basic purpose of program semantics is to give a rigorous, unambiguous definition of the meaning of programs, providing a standard for translator writers and users of the language. Beyond this basic purpose, equality and other relations on program fragments can be defined, leading to logics for reasoning about programs and formal justification for program transformations. In the last twenty-five years, tremendous progress has been made. The most important step was the development of semantic domains to denotationally model programs, which have since been extended to model the constructs of modern languages such as assignments, branches and nondeterminism. Logics for reasoning about programs have also been defined for simple languages, using semantic domains as models to guarantee soundness. The difficulty is scaling up these ideas to full-fledged languages with many features. Operational semantics provides an alternative to denotational semantics here, because there is always at the bottom an interpreter, keeping ones feet on the ground, and keeping the mathematics manageable. This project takes an operational approach to semantics, with the aim of giving semantics to full-fledged programming languages and to furthermore define a rich notion of eqivalence of programs so logics can thereupon be defined. This undertaking is thus a synthesis of many different varieties of language semantics.