Commit 239fc3d9 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

'equivalence' lemma for the two semantics (actually just an implication)

parent 26b72929
......@@ -183,7 +183,7 @@
{}
\end{mathpar}
We denote by $e\uleadsto e'$ a step of reduction of the parallel semantic, regardless of the value on the top of the arrow.
We denote by $e\uleadsto e'$ a step of reduction of the parallel semantics, regardless of the value on the top of the arrow.
\[\valsemantic t = \{v \alt \vvdash v : t\}\]
......@@ -205,6 +205,20 @@
\\
\end{mathpar}
All the proofs below will use the parallel semantics instead of the standard semantics (\ref{sec:opsem}).
However, the safety of the type system for the standard semantics can be deduced from the safety of the type system for the parallel semantics,
using the following lemma:
\begin{lemma}\label{semanticsimpl}
$\forall e, v.\ e\uleadsto^* v \Rightarrow e\reduces^* v$
\end{lemma}
\begin{proof}
The additional substitutions made by the rule \Rule{TestCtx} will be performed later with the standard semantics.
This relies on the fact that our language is pure.
\end{proof}
The reciproque is also true, but is not needed to prove the safety of the type system.
\subsection{Proofs for the declarative type system}\label{app:soundness}
In this section, the substitutions on expressions that we introduce are up to alpha-renaming and perform only one pass.
......
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