Commit abe3058e authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Moving to functional choreographies.

parent 37855c7e
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -9,26 +9,26 @@ Module SoundlyTypedChoreography (E : Expression) (TE : TypedExpression E) (STE :
Include (TypedChoreography L E TE).
Theorem Preservation :
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> L.t * ExprTyp) (C : Chor) (τ : ExprTyp) (p : L.t),
Γ;; Δ c C ::: τ @ p -> forall (R : Redex) (B : list L.t) (C': Chor),
RChorStep R B C C' -> Γ;; Δ c C' ::: τ @ p.
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
Γ;; Δ c C ::: τ -> forall (R : Redex) (B : list L.t) (C': Chor),
RChorStep R B C C' -> Γ;; Δ c C' ::: τ.
Proof.
apply RelativePreservation. intros Γ e τ H e' H0.
apply ExprPreservation with (e1 := e); auto.
Qed.
Theorem CompletePreservation:
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> L.t * ExprTyp) (C : Chor) (τ : ExprTyp) (p : L.t),
Γ;; Δ c C ::: τ @ p -> forall (R : Redex) (B : list L.t) (C': Chor),
CompleteRChorStep R B C C' -> Γ;; Δ c C' ::: τ @ p.
forall (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (C : Chor) (τ : ChorTyp),
Γ;; Δ c C ::: τ -> forall (R : Redex) (B : list L.t) (C': Chor),
CompleteRChorStep R B C C' -> Γ;; Δ c C' ::: τ.
Proof.
apply CompleteRelativePreservation. intros Γ e τ H e' H0.
apply ExprPreservation with (e1 := e); auto.
Qed.
Theorem Progress :
forall (C : Chor) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> L.t * ExprTyp) (τ : ExprTyp) (p : L.t),
ChorClosed C -> Γ;; Δ c C ::: τ @ p ->
forall (C : Chor) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
ChorClosed C -> Γ;; Δ c C ::: τ ->
ChorVal C \/ exists R C', RChorStep R nil C C'.
Proof.
apply RelativeProgress; auto.
......@@ -37,8 +37,8 @@ Module SoundlyTypedChoreography (E : Expression) (TE : TypedExpression E) (STE :
Qed.
Theorem CompleteProgress :
forall (C : Chor) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> L.t * ExprTyp) (τ : ExprTyp) (p : L.t),
ChorClosed C -> Γ;; Δ c C ::: τ @ p ->
forall (C : Chor) (Γ : L.t -> nat -> ExprTyp) (Δ : nat -> ChorTyp) (τ : ChorTyp),
ChorClosed C -> Γ;; Δ c C ::: τ ->
ChorVal C \/ exists R C', CompleteRChorStep R nil C C'.
Proof.
apply CompleteRelativeProgress; auto.
......
This diff is collapsed.
......@@ -11,6 +11,3 @@ FunLMap.v
Choreography.v
TypedChoreography.v
SoundlyTypedChoreography.v
ProcessCalculus.v
InternalProcesses.v
ChoreographyCompiler.v
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment