On affine usages in signal-based communication
Roberto Amadio (PPS), Mehdi Dogguy (PPS)
TL;DR
This paper introduces a type system for a synchronous pi-calculus that formalizes affine usage in signal communication, ensuring programs are deterministic by design.
Contribution
It defines a limited set of affine usages that can be composed, and proves that typable programs are deterministic.
Findings
Typable programs are deterministic.
A formal system for affine usages in signal communication.
Composability of affine usages.
Abstract
We describe a type system for a synchronous pi-calculus formalising the notion of affine usage in signal-based communication. In particular, we identify a limited number of usages that preserve affinity and that can be composed. As a main application of the resulting system, we show that typable programs are deterministic.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Computability, Logic, AI Algorithms