Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • A Actris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 5
    • Issues 5
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 2
    • Merge requests 2
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • Actris
  • Issues
  • #6
Closed
Open
Created Apr 15, 2020 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 Apr 25, 2020 by Jonas Kastberg
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking