You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Naso (Aug 22 2023 at 04:21):Hey Everyone :tada:,
I'm excited to share our paper, "Trace models of concurrent valuation algebras," that was recently accepted at ICFEM23 in my hometown Brisbane, Australia. A freshly revised version (v3) is now on arXiv.
Abstract: This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and sequential products, adhering to a weak exchange law. This development offers theoretical and practical benefits for the specification and modelling of concurrent and distributed systems. As a presheaf on a space of domains, CVAs enable localised specifications, supporting modularity, compositionality, and the ability to represent large and complex systems. Furthermore, CVAs align with lattice-based refinement reasoning and are compatible with established methodologies such as Hoare and Rely-Guarantee logics. The flexibility of CVAs is explored through three trace models, illustrating distinct paradigms of concurrent/distributed computing, interrelated by morphisms. The paper also highlights the potential to incorporate a powerful local computation framework from valuation algebras for model checking in concurrent and distributed systems. The foundational results presented have been verified with the proof assistant Isabelle/HOL.
A significant part of the paper (Sections 2,3,4,6) is formalised in the proof assistant Isabelle/HOL. You can find the code here. A word of warning though, this was my first project with Isabelle, so my approach may be a bit unorthodox! :upside_down:
I can't let this moment pass without expressing my heartfelt gratitude to this incredible community. Your friendship, support, and invaluable insights have directly contributed to this paper. Thank you! :pray:
(On a more personal note, and I hope it's okay to mention this here, I'm approaching the end of my PhD journey and am actively looking for work. I'm open to remote opportunities and relocation. If you have any leads or want to collaborate, feel free to reach out!)
Wishing you all the best!