GitLab

We need to make sure that we have all the subtyping rules.

All rules that have been added to the paper, but are not yet formalised are unticked here:

• Dual left/right
• Dual unfoldings of send/receive: dual <!> A. S <: <?> A. dual S, <!> A. dual S <: dual <?> A. S etc.
• Dual unfoldings of select/branch
• Unfoldings of append
• Append associativity rules
• Append identity rules
• Swap rule for select/recv
• Swap rule for send/branch
• Swap rule for select/branch
• Forall elimination: ∀X.A <: A[K/X] (Needs update to ∀ with value restriction)
• Exist elimination: A[K/X] <: ∃X.A
• Update Send rule with quantifiers
• Update Recv rule with quantifiers
• Send rule for quantifier instantiation: chan !{X, X}A.S <: chan !{X}A[K/X].S[K/X]
• Recv rule for quantifier instantiation: chan ?{X}A[K/X].S[K/X] <: chan ?{X, X}A.S