ICE-TCS seminar: Niccolò Veltri

Formalizing π-Calculus in Guarded Cubical Agda

  • 17.2.2020, 11:50 - 12:35

ICE-TCS-logo-200px

ICE-TCS seminar #348

Date and time: Monday, 17 January 2020, 11:50-12:35
Location: Room M108
Speaker: Niccolò Veltri, Tallinn University of Technology, Estonia https://niccoloveltri.github.io/

Title: Formalizing π-Calculus in Guarded Cubical Agda

Abstract: 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 has been used to show that, for labelled transition systems, 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 labelled transition systems.

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.

Joint work with Andrea Vezzosi.



Vinsamlegast athugið að á viðburðum Háskólans í Reykjavík (HR) eru teknar ljósmyndir og myndbönd sem notuð eru í markaðsstarfi HR. Hægt er að nálgast frekari upplýsingar á ru.is eða með því að senda tölvupóst á netfangið: personuvernd@ru.is
//
Please note that at events hosted at Reykjavik University (RU), photographs and videos are taken which might be used for RU marketing purposes. Read more about this on our ru.is or send an e-mail: personuvernd@ru.is