Email Gateway (Sep 28 2026 at 15:56): Email Gateway (Sep 28 2026 at 15:56):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP (devel): IMP_concur - A Semantics for a Language with Concurrency based on HOL-CSP
Currently only available in the development version, and soon in the
release AFP for the upcoming Isabelle 2026.
IMP_concur -ASemantics for aLanguage withConcurrency based onHOL-CSP
Burkhart Wolff
August 31, 2026
Abstract
The theory IMPconcur provides a programming-language aspect to HOL-CSP.
It extends the well-known imperative language IMP originated by Glenn
Winskell by concurrent primitives like lock and unlock for semaphores,
thread-local and system global program variables and the notion of
threads that run in interleaving semantics. Threads can be parametric
and used to construct concurrent process architectures. Representing
IMPconcur semantics can be done by a straight-forward translation into
HOL-CSP; thus, IMPconcur can be seen as a thin layer on top of the
theory of Concurrent Sequential Processes of Hoare, Brookes and Roscoe
in its formalization HOL-CSP in Isabelle/HOL. Notwithstanding its
simplicity, IMPconcur covers many aspects of concurrency,
non-termination, divergence, synchronization, states and
race-conditions. We believe that IMPconcur may be relevant for readers
interested in the link between programming languages and process
algebras. Resulting new ways to concurrent program verification are an
interesting target for future study. We also present a language
extension for dynamic reconfigurations of thread- architectures. This
session is complemented by a syntactic frontend for IMPconcur, called
CIL, which has been authored by Mathilde Needham and Zineddine Kermadj
on their internship project in summer 2025.
Enjoy!
Last updated: Oct 08 2026 at 21:07 UTC