一句话：提出融合博弈语义、精化演算与代数效应的统一框架，以嵌入并组合经机器验证的抽象层及证明。
形式化方法已能机械验证大型系统组件的功能正确性，但不同项目采用多样的语义模型，导致已验证组件难以组合成更大的认证系统。本文旨在将这些模型与证明嵌入一个可交互的通用框架，并提出以博弈语义、精化演算和代数效应的综合作为实现方案：博弈语义刻画组件与环境的交互，精化演算支持抽象层间的逐步精化与证明复用，代数效应统一处理计算效应。作者认为该综合可为认证抽象层提供统一的语义与推理基础，从而支持构建更大规模的可信系统。摘要未报告具体实现或实验评估。
Formal methods have advanced to the point where the functional correctness of various large system components has been mechanically verified. However, the diversity of semantic models used across projects makes it difficult to connect these component to build larger certified systems. Given this, we seek to embed these models and proofs into a generalpurpose framework where they could interact. We believe that a synthesis of game semantics, the refinement calculus, and algebraic effects can provide such a framework.
DOI 原文 ·
@inproceedings{paperbot5498,
title = {Refinement-Based Game Semantics for Certified Abstraction Layers},
author = {Jérémie Koenig and Zhong Shao},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394799}
}