Write a Blog >>
Tue 21 Jan 2020 14:21 - 14:43 at Maurepas - Concurrency and linearity Chair(s): Zhong Shao

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.

Slides (slides-cpp20.pdf)163KiB

Tue 21 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

14:00 - 15:05: CPP 2020 - Concurrency and linearity at Maurepas
Chair(s): Zhong ShaoYale University
CPP-2020-papers14:00 - 14:21
Roy OverbeekVrije Universiteit Amsterdam
DOI Pre-print Media Attached
CPP-2020-papers14:21 - 14:43
Niccolò VeltriTallinn University of Technology, Andrea VezzosiIT University Copenhagen
DOI Pre-print Media Attached File Attached
CPP-2020-papers14:43 - 15:05
Arjen RouvoetDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology
DOI Pre-print Media Attached File Attached