Formalizing 휋-calculus in guarded cubical Agda

Niccolò Veltri; Andrea Vezzosi

doi:10.1145/3372885.3373814

Formalizing 휋-calculus in guarded cubical Agda

Niccolò Veltri, Andrea Vezzosi

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

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 (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.

Originalsprog	Engelsk
Titel	CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs ACM
Antal sider	14
Forlag	Association for Computing Machinery
Publikationsdato	2020
Sider	270-283
ISBN (Trykt)	9781450370974
DOI	https://doi.org/10.1145/3372885.3373814
Status	Udgivet - 2020
Begivenhed	9th ACM SIGPLAN International Conference on Certified Programs and Proofs - Varighed: 20 jan. 2020 → … https://popl20.sigplan.org/home/CPP-2020

Konference

Konference	9th ACM SIGPLAN International Conference on Certified Programs and Proofs
Periode	20/01/2020 → …
Internetadresse	https://popl20.sigplan.org/home/CPP-2020

Emneord

Dependent type theories
Guarded recursion
Denotational semantics
π-calculus
Guarded Cubical Agda

Adgang til dokumentet

10.1145/3372885.3373814

Formalizing 𝜋-calculus in guarded cubical AgdaAccepteret manuskript, 289 KB

Type theories for reactive programming
Møgelberg, R. E. (PI), Vezzosi, A. (CoI), Graulund, C. U. (CoI), Kristensen, M. B. (CoI) & Veltri, N. (CoI)
Villum Fonden
22/01/2016 → 21/01/2022
Projekter: Projekt › Forskning

Citationsformater

@inproceedings{80d3b38f59e84776817dc419fc7e5d11,

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 (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.",

keywords = "Dependent type theories, Guarded recursion, Denotational semantics, π-calculus, Guarded Cubical Agda, Dependent type theories, Guarded recursion, Denotational semantics, π-calculus, Guarded Cubical Agda",

author = "Niccol{\`o} Veltri and Andrea Vezzosi",

year = "2020",

doi = "10.1145/3372885.3373814",

language = "English",

isbn = "9781450370974",

pages = "270--283",

booktitle = "CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs ACM",

publisher = "Association for Computing Machinery",

address = "United States",

note = "9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP2020 ; Conference date: 20-01-2020",

url = "https://popl20.sigplan.org/home/CPP-2020",

}

Formalizing 휋-calculus in guarded cubical Agda. / Veltri, Niccolò; Vezzosi, Andrea.
CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs ACM. Association for Computing Machinery, 2020. s. 270-283.

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - Formalizing 휋-calculus in guarded cubical Agda

AU - Veltri, Niccolò

AU - Vezzosi, Andrea

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - Dependent type theories

KW - Guarded recursion

KW - Denotational semantics

KW - π-calculus

KW - Guarded Cubical Agda

KW - Dependent type theories

KW - Guarded recursion

KW - Denotational semantics

KW - π-calculus

KW - Guarded Cubical Agda

U2 - 10.1145/3372885.3373814

DO - 10.1145/3372885.3373814

M3 - Article in proceedings

SN - 9781450370974

SP - 270

EP - 283

BT - CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs ACM

PB - Association for Computing Machinery

T2 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

Y2 - 20 January 2020

ER -

Formalizing 휋-calculus in guarded cubical Agda

Abstract

Konference

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

Type theories for reactive programming

Citationsformater