The paper gives a detailed presentation of a framework, embedded into the simply typed higher-order logic and aimed at the support of sound and structured reasoning about various properties of models of imperative programs with interleaved computations. As a case study, a model of the Peterson's mutual exclusion algorithm will be scrutinised in the course of the paper illustrating applicability of the framework.

翻译：本文详细阐述了一个嵌入简单类型高阶逻辑的框架，旨在为具有交错计算的命令式程序模型的各种属性提供可靠且结构化的推理支持。作为案例研究，文中将通过详细审视Peterson互斥算法模型来论证该框架的适用性。