skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


This content will become publicly available on August 19, 2026

Title: A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga
Reversible concurrent calculi are abstract models for concurrent systems in which any action can potentially be undone. Over the last few decades, different formalisms have been developed and their mathematical properties have been explored; however, none have been machine-checked within a proof assistant. This paper presents the first Beluga formalization of the Calculus of Communicating Systems with Keys and Proof labels (CCSKP), a reversible extension of CCS. Beyond the syntax and semantics of the calculus, the encoding covers state-of-the-art results regarding three relations over proof labels – namely, dependence, independence and connectivity – which offer new insights into the notions of causality and concurrency of events. As is often the case with formalizations, our encoding introduces adjustments to the informal proof and makes explicit details which were previously only sketched, some of which reveal to be less straightforward than initially assumed. We believe this work lays the foundations for future reversible concurrent calculi formalizations.  more » « less
Award ID(s):
2242786
PAR ID:
10658097
Author(s) / Creator(s):
 
Editor(s):
Aubert, Clément; Di_Giusto, Cinzia; Fowler, Simon; Ka_I_Pun, Violet
Publisher / Repository:
Electronic Proceedings in Theoretical Computer Science
Date Published:
Journal Name:
Electronic Proceedings in Theoretical Computer Science
Volume:
425
ISSN:
2075-2180
Page Range / eLocation ID:
55 to 72
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. (, Journal of Logical and Algebraic Methods in Programming)
    Claudio Antares Mezzina (Ed.)
    This article designs a general principle to check the correctness of the definition of concurrency (a.k.a. independence) of events for concurrent calculi. Concurrency relations are central in process algebras, but also two-sided: they are often defined independently on composable and on coinitial transitions, and no criteria exist to assess whether they “interact correctly”. This article starts by examining how reversibility can provide such a correctness of concurrencies criterion, and its implications. It then defines, for the first time, a syntactical definition of concurrency for CCSK, a reversible declension of the calculus of communicating systems. To do so, according to our criterion, requires to define concurrency relations for all types of transitions along two axes: direction (forward or backward) and concomitance (coinitial or composable). Our definition is uniform thanks to proved transition systems and satisfies our sanity checks: square properties, sideways diamonds, but also the reversible checks (reverse diamonds and causal consistency). We also prove that our formalism is either equivalent to or a refinement of pre-existing definitions of concurrency for reversible systems. We conclude by discussing additional criteria and possible future works. 
    more » « less
  2. ; ; (, Springer Nature Switzerland)
    Glück, Robert; Kaarsgaard, Robin (Ed.)
    Among the formalisms that can be used to reason about concurrent systems, process calculi stand out both for their simple syntax and close connection to reversibility. They also offer approaches to study relations such as dependence, concurrency or causality between transitions, useful in exploring e.g., causes of bugs or how to multi-thread executions. This paper offers two main contributions: first, we provide separate definitions of a dependence relation and an independence relation, and prove their complementarity on connected transitions instead of postulating it, as is usually done. We also prove that those relations, as well as the notions of event, concurrency, causality and conflict, are unique for any reversible system respecting basic sanity axioms. Second, we prove that the operational definitions of core independence and causality coincide with their characterisations using a pre-existing syntactic mechanism in reversible process calculi, namely communication keys. 
    more » « less
  3. ; (, Journal of Functional Programming)
    Abstract The research on gradual typing has led to many variations on the Gradually Typed Lambda Calculus (GTLC) of Siek & Taha (2006) and its underlying cast calculus. For example, Wadler and Findler (2009) added blame tracking, Siek et al . (2009) investigated alternate cast evaluation strategies, and Herman et al . (2010) replaced casts with coercions for space efficiency. The meta-theory for the GTLC has also expanded beyond type safety to include blame safety (Tobin-Hochstadt & Felleisen, 2006), space consumption (Herman et al ., 2010), and the gradual guarantees (Siek et al ., 2015). These results have been proven for some variations of the GTLC but not others. Furthermore, researchers continue to develop variations on the GTLC, but establishing all of the meta-theory for new variations is time-consuming. This article identifies abstractions that capture similarities between many cast calculi in the form of two parameterized cast calculi, one for the purposes of language specification and the other to guide space-efficient implementations. The article then develops reusable meta-theory for these two calculi, proving type safety, blame safety, the gradual guarantees, and space consumption. Finally, the article instantiates this meta-theory for eight cast calculi including five from the literature and three new calculi. All of these definitions and theorems, including the two parameterized calculi, the reusable meta-theory, and the eight instantiations, are mechanized in Agda making extensive use of module parameters and dependent records to define the abstractions. 
    more » « less
  4. (, Proceedings of the ACM on Programming Languages)
    Dependency analysis is vital to several applications in computer science. It lies at the essence of secure information flow analysis, binding-time analysis, etc. Various calculi have been proposed in the literature for analysing individual dependencies. Abadi et. al., by extending Moggi’s monadic metalanguage, unified several of these calculi into the Dependency Core Calculus (DCC). DCC has served as a foundational framework for dependency analysis for the last two decades. However, in spite of its success, DCC has its limitations. First, the monadic bind rule of the calculus is nonstandard and relies upon an auxiliary protection judgement. Second, being of a monadic nature, the calculus cannot capture dependency analyses that possess a comonadic nature, for example, the binding-time calculus, λ∘, of Davies. In this paper, we address these limitations by designing an alternative dependency calculus that is inspired by standard ideas from category theory. Our calculus is both monadic and comonadic in nature and subsumes both DCC and λ∘. Our construction explains the nonstandard bind rule and the protection judgement of DCC in terms of standard categorical concepts. It also leads to a novel technique for proving correctness of dependency analysis. We use this technique to present alternative proofs of correctness for DCC and λ∘. 
    more » « less
  5. (, Zenodo)
    This artifact contains the source code for the paper "A Formalization of the Reversible Concurrent Calculus CCSK^P in Beluga" (ICE 2025). 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email