An Agda formalization of the Calculus of Communicating Systems

This is a formalization of CCS, done for my master’s thesis “Bisimulation-Based Process Algebra in Higher-Order GSOS”. It implements a version of the calculus with finite sums and arbitrary fixpoints. Variables are represented via de Bruijn indices, in a style akin to Programming Language Foundations in Agda. The main result is the definition of a coalgebra $γ$ with the HO-GSOS framework layed out in Higher-Order Mathematical Operational Semantics.

Browse the source code on https://flogth.github.io/ccs