Errata in the LiCS 2007 Paper

Andreas Abel May 12, 2008

Theorem 12 is proves more that we actually need. It is sufficient to show that all well-typed terms are in the logical relation. Nothing needs to be shown about judgemental equality, since we have constructed a per model for it already.

Thus, it is sufficient to prove: Theorem 12 (Fundamental theorem of logical relations)

1. If Γ ⊢ t : A then Δ ⊢ t[σ] : A[σ] ◯^{R} [[t]]_{ρ} ∈ [[A]]_{ρ} for all Δ ⊢ σ : Γ ◯^{R} ρ.

2. If Γ ⊢ A then Δ ⊢ A[σ] ◯^{R} [[A]]_{ρ} for all Δ ⊢ σ : Γ ◯^{R} ρ. Proof. Each by induction on the derivation. □