Isabelle中是否存在面向命令式语言的并发分离逻辑框架？

针对你寻找类似Coq/Iris、面向C类并发命令式语言的Isabelle框架需求，以下是几个关键选项：

• Viktor Vafeiadis的并发分离逻辑实现：这是Isabelle生态中最贴合需求的早期工作，支持并发命令式程序的核心推理特性，包括线程间的所有权管理、锁的模块化验证等。后续基于此的衍生优化版本在AFP（Archive of Formal Proofs）中可查，部分版本改进了语法易用性。

• Imperative HOL的并发扩展：你提到的分离逻辑框架虽原生面向顺序程序，但已有AFP条目对其进行并发扩展，实现了对C风格并发特性（如线程创建、原子操作、共享内存）的推理支持，可作为基础扩展使用。

• AFP上的现代化并发分离逻辑框架：近年归档的部分条目（如标注为Concurrent_Separation_Logic的相关工作）提供了更友好的语法接口，借鉴了Iris的高阶抽象设计，支持自定义断言、并发原语的模块化验证，能满足复杂并发场景的细致特性需求。

内容的提问来源于stack exchange，提问作者Huan Sun