Formalizing pi-Calculus in Guarded Cubical Agda
summary
Implements guarded extensions of Cubical Agda and formalizes an internal denotational model of the early pi-calculus; builds a higher-inductive finite powerset to model nondeterminism and a guarded recursion domain of semantic processes (sets of labeled transitions available only later); proves full soundness and completeness with respect to early congruence (behavioral equivalence) and mechanizes the development in the prototype extended Cubical Agda, with typechecking and proofs completed for the presented fragments.
AI-written summary · about
chapters (7)
- 0:00Introduction and motivation
- 2:55Cubical and higher types
- 5:55Guarded recursion basics
- 8:42Pi calculus formalization
- 12:45Constructing the domain
- 16:54Conclusion and future work
- 19:02Questions and answers
related talks
01h 07mAn introduction to synthetic guarded domain theory with applications to probabilistic(…)
23mCo-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
20mModal Mu-Calculus for Free in Agda
26mTemporal refinements for Call-By-Push-Value with fixpoint
22mA Calculus of Inductive Linear Constructions
25mCall-Guarded Abstract Definitional Interpreters
30mPlausible sealing for gradual parametricity