Skip to content

GitLab

Open
Created by Jonas Kastberg@jihgfeeMaintainer9 of 15 tasks completed9/15 tasks

Finish up Subtyping

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
Edited by Jonas Kastberg
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information