SoundlyTypedChoreography.v 1.13 KB
Newer Older
1
2
Require Export Choreography.
Require Export TypedChoreography.
3
4
5
6
Require Export Expression.
Require Export TypedExpression.
Require Export SoundlyTypedExpression.

7
Module SoundlyTypedChoreography (E : Expression) (TE : TypedExpression E) (STE : SoundlyTypedExpression E TE) (L : Locations).
8
  Import E. Import TE. Import STE.
9
  Include (TypedChoreography L E TE).
10
11


12
    Theorem Preservation:
13
14
      forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
        Γ;; Δ c C ::: τ -> forall (R : Redex) (B : list L.t) (C': Chor),
15
          ChorStep R B C C' -> Γ;; Δ c C' ::: τ.
16
    Proof.
17
      apply RelativePreservation. intros Γ e τ H e' H0.
18
19
20
      apply ExprPreservation with (e1 := e); auto.
    Qed.

21
    Theorem Progress :
22
23
    forall (C : Chor) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
      ChorClosed C -> Γ;; Δ c C ::: τ ->
24
      ChorVal C \/ exists R C', ChorStep R nil C C'.
25
26
27
28
29
    Proof.
      apply RelativeProgress; auto.
      intros e τ Γ H H0; eapply ExprProgress; eauto.
      intros v Γ H H0; eapply BoolInversion; eauto.
    Qed.
30

31
32
33
End SoundlyTypedChoreography.