Commit 30b0b2d0 authored by Amin Timany's avatar Amin Timany
Browse files

coqdoc for compatibility.v

parent af43752f
From tutorial_popl20 Require Export sem_typed sem_operators.
(** * Compatibility of logical relations with typing rules.
Here we prove that the logical relations, i.e., the semantic
typing judgment, that we have defined is compatible with typing
rules. That is, the logical relations is a congruence with respect
to the typing rules.
These compatibility lemmas are what one gets when the syntactic
typing judgment is replaced semantic typing judgment in syntactic
typing rules. For instance ([sem_typed_pair]):
<<
Γ ⊢ e1 : T1 Γ ⊢ e2 : T2
--------------------------------
Γ ⊢ (e1, e2) : T1 × T2
>>
becomes
<<
(Γ ⊨ e1 : T1) -∗ (Γ ⊨ e2 : T2) -∗ Γ ⊢ (e1, e2) : T1 × T2
>>
*)
Section compatibility.
Context `{heapG Σ}.
Implicit Types A B : sem_ty Σ.
......
Markdown is supported
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