Formalizing π-calculus in Guarded Cubical Agda
Dependent type theories with guarded recursion have shown themselves suitable for the development of denotational semantics of programming languages. In particular Ticked Cubical Type Theory (TCTT) has been used to show that for guarded labelled transition systems (GLTS) interpretation into the denotational semantics maps bisimilar processes to equal values. In fact the two notions are proved equivalent, allowing one to reason about equality in place of bisimilarity.
We extend that result to the $\pi$-calculus, picking early congruence as the syntactic notion of equivalence between processes, showing that denotational models based on guarded recursive types can handle the dynamic creation of channels that goes beyond the scope of GLTSs.
Hence we present a fully abstract denotational model for the early $\pi$-calculus, formalized as an extended example for Guarded Cubical Agda: a novel implementation of Ticked Cubical Type Theory based on Cubical Agda.
Tue 21 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
Concurrency and linearityCPP at Maurepas
Chair(s): Zhong Shao Yale University
|Formalizing Determinacy of Concurrent Revisions|
Roy Overbeek Vrije Universiteit AmsterdamDOI Pre-print Media Attached
|Formalizing π-calculus in Guarded Cubical Agda|
Niccolò Veltri Tallinn University of Technology, Andrea Vezzosi IT University CopenhagenDOI Pre-print Media Attached File Attached
|Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages|
Arjen Rouvoet Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Delft University of Technology, Eelco Visser Delft University of TechnologyDOI Pre-print Media Attached File Attached