Pat is the first actor programming language with mailbox types that enable static detection of four classes of behavioral errors plus ordinary type errors via an algorithmic type system proven sound and complete.
In Eike Best, editor: CONCUR’93
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
fields
cs.PL 3representative citing papers
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.
Effpi gains branching for existential external choice across channels plus timeout handling to support more expressive typed message-passing protocols such as Raft.
citing papers explorer
-
Special Delivery: Programming with Mailbox Types (Extended Version)
Pat is the first actor programming language with mailbox types that enable static detection of four classes of behavioral errors plus ordinary type errors via an algorithmic type system proven sound and complete.
-
Logical Relations for Session-Typed Concurrency
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.
-
Branching Out: Existential External Choice in Effpi
Effpi gains branching for existential external choice across channels plus timeout handling to support more expressive typed message-passing protocols such as Raft.