Guarantees by Construction (Mechanization)

Jules Jacobs

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
(** 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.
Proof.
  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.
Qed.