Research Initiation: Semantics and Logics of Programs

程序语义学最基本的目的是对程序的意义给出一个严格、明确的定义，为译者、作者和语言使用者提供一个标准。除了这个基本目的之外，还可以定义程序片段上的相等和其他关系，从而导致程序推理的逻辑和程序转换的形式证明。在过去的25年里，取得了巨大的进步。最重要的一步是开发语义域来对程序进行指示性建模，这已经扩展到对现代语言的结构（如赋值、分支和不确定性）进行建模。对于简单的语言，也定义了程序推理的逻辑，使用语义域作为模型来保证可靠性。难点在于将这些想法扩展为具有许多功能的成熟语言。操作语义在这里提供了指称语义的另一种选择，因为在底层总是有一个解释器，使人脚踏实地，并使数学易于管理。这个项目对语义采取了一种可操作的方法，其目的是为成熟的编程语言提供语义，并进一步定义程序对等的丰富概念，从而可以定义逻辑。因此，这项工作是许多不同种类的语言语义学的综合。

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.