一句话：以第一性原理统一、完整地阐述 Iris 3.1 的设计与语义基础，为高阶并发分离逻辑奠定模块化框架。
Iris 是一个在 Coq 证明助手中实现的高阶并发分离逻辑框架，已被广泛应用于各类程序验证项目。它的设计初衷是简化并整合现代分离逻辑的基础，但随着版本不断演化，Iris 自身的设计与语义基础始终没有被完整地记录并在同一处加以系统解释。本文旨在填补这一空白：作者以第一性原理出发，采用连贯统一的叙述方式，从头呈现最新版本 Iris（3.1）的完整图景，涵盖其模块化基础的核心构成与整体架构。文章并非提出新的逻辑系统或新的验证工具，而是一篇奠基性的、教科书式的系统阐述，使读者能够理解 Iris 为何如此设计、其语义基础如何组织，以及这种模块化基础如何支撑其在高阶并发分离逻辑中的广泛适用性。
Iris is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.
@article{paperbot343,
title = {Iris from the ground up: A modular foundation for higher-order concurrent separation logic},
author = {RALF JUNG and ROBBERT KREBBERS and JACQUES-HENRI JOURDAN and ALEŠ BIZJAK and LARS BIRKEDAL and DEREK DREYER},
journal = {Journal of Functional Programming},
volume = {28},
year = {2018},
doi = {10.1017/s0956796818000151}
}