Caos: A Reusable Scala Web Animator of Operational Semantics (Extended With Hands-On Tutorial)
Jos\'e Proen\c{c}a, Luc Edixhoven

TL;DR
Caos is a Scala-based framework that facilitates the design, visualization, and animation of structural operational semantics for formal models, enabling early detection of errors and insights during development.
Contribution
It introduces a reusable Scala library and workflow for designing and visualizing operational semantics, bridging theory and practical tool development.
Findings
Successfully applied to analyze a simple while-language
Used for choreographic language semantics analysis
Enabled early detection of mistakes and limitations
Abstract
This tool paper presents Caos: a methodology and a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach in which theoretical foundations and a practical tool are built together, as an alternative to foundations-first design ("tool justifies theory") or tool-first design ("foundations justify practice"). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. We share two…
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.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsData Visualization and Analytics · Logic, programming, and type systems
