ITU

Formalizing 휋-calculus in guarded cubical Agda

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

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 π-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 π-calculus, formalized as an extended example for Guarded Cubical Agda: a novel implementation of Ticked Cubical Type Theory based on Cubical Agda.
Original languageEnglish
Title of host publicationCPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs ACM
Number of pages14
PublisherAssociation for Computing Machinery
Publication date2020
Pages270-283
ISBN (Print)9781450370974
DOIs
Publication statusPublished - 2020
Event9th ACM SIGPLAN International Conference on Certified Programs and Proofs -
Duration: 20 Jan 2020 → …
https://popl20.sigplan.org/home/CPP-2020

Conference

Conference9th ACM SIGPLAN International Conference on Certified Programs and Proofs
Periode20/01/2020 → …
Internetadresse

Downloads

No data available

ID: 84931954