A Framework for Concurrent Imperative Programming
Stephan van Staden

TL;DR
This paper introduces a general algebraic framework for concurrent imperative programming, modeling programs as formal languages and concurrency as an interleaving operator, supporting various program logics and operational calculi.
Contribution
It presents a simple, mathematically straightforward model that unifies different approaches to concurrent programming and correctness verification.
Findings
Validates program logic consistency without induction
Supports multiple concrete languages and settings
Provides a unified algebraic framework for concurrency
Abstract
The proposed framework provides a general model of concurrent imperative programming. Programs are modeled as formal languages and concurrency as an interleaving (or shuffle) operator. This yields a simple and elegant algebra of programs. The framework supports the views program logic by Dinsdale-Young and others, which generalizes various type systems and separation logic approaches to program correctness. It also validates familiar operational calculi in small-step and big-step flavours. The consistency of the program logic with respect to the operational rules is established directly and does not use induction on derivations. In fact the whole framework uses only straightforward mathematics. Parametric in states, views and basic commands, it can be instantiated to a variety of concrete languages and settings.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Parallel Computing and Optimization Techniques
