Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing (Artifact)

Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers

(** This file contains shows that the program

  λ c, (recv c, recv c)

can be assigned the type

  chan (?int.?int.end) ⊸ (int * int)

by exclusively using the semantic typing rules. *)
From dlfactris.session_logic Require Import proofmode.
From dlfactris.logrel Require Export term_typing_rules session_typing_rules.

Definition prog : expr :=
  λ: "c", let: "xy" := (recv "c", recv "c") in wait "c";; "xy".

Lemma prog_typed :
  []  prog : chan (<??> TY lty_int; <??> TY lty_int; END??)  lty_int * lty_int.
  iApply (ltyped_lam []).
  iApply ltyped_subsumption_alt;
    [by iApply ctx_le_refl| |by iApply lty_le_refl|].
  { iApply ltyped_let.
    { iApply ltyped_pair.
      - by iApply ltyped_recv.
      - by iApply ltyped_recv. }
    iApply ltyped_seq; [by iApply lty_copyable_unit|by iApply ltyped_wait|].
    by iApply ltyped_var. }
  iApply ctx_le_drop. iApply lty_copyable_copy_inv.