Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda

DOI10.1016/j.jlamp.2022.100846OpenAlexW4313529991MaRDI QIDQ2683037

Andrea Vezzosi, Niccolò Veltri

Publication date: 3 February 2023

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2022.100846

zbMATH Keywords

denotational semantics\(\pi\)-calculusguarded recursionticked cubical type theory

Mathematics Subject Classification ID

Computer science (68-XX)

Related Items (2)

Cubical methods in homotopy type theory and univalent foundations ⋮ Streams of approximations, equivalence of recursive effectful programs

Uses Software

• Celf
• cubicaltt

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal logics for mobile processes
• A calculus of communicating systems
• A calculus of mobile processes. I
• \(\pi\)-calculus in (Co)inductive-type theory
• An algorithm for type-checking dependent types
• Guarded cubical type theory
• Guarded Dependent Type Theory with Coinductive Types
• Formalising the pi-calculus using nominal logic
• Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
• Second-Order Algebraic Theories
• Quotienting the delay monad by weak bisimilarity
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Denotational semantics of recursive types in synthetic guarded domain theory
• Proof-relevant π-calculus: a constructive account of concurrency and causality
• On Higher Inductive Types in Cubical Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• A model of PCF in guarded type theory

This page was built for publication: Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda