coercion semantics

paper/main.tex

@@ -116,6 +116,13 @@ $$\\$$
 	{ \metavariable{x}
 } {Variable}
 
+\otherform{
+	\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad 
+	\nonterm{ E }
+	\quad \exprterminal{in} \quad
+	\nonterm{ E }
+}{Variable Binding}
+
 \otherform{
 	$$ \exprterminal{\Lambda} \metavariable{\alpha}
 	\quad \exprterminal{\mapsto} \quad $$
@@ -136,13 +143,6 @@ $$\\$$
 	\nonterm{ E }
 }{Value Morphism}
 
-\otherform{
-	\exprterminal{let} \quad \metavariable{x} \quad \exprterminal{=} \quad 
-	\nonterm{ E }
-	\quad \exprterminal{in} \quad
-	\nonterm{ E }
-}{Variable Binding}
-
 \otherform{
 	\nonterm{ E }
 	\quad
@@ -161,23 +161,25 @@ $$\\$$
 	\exprterminal{as}
 	\quad
     \nonterm{ T }
-}{Up-Cast}
+}{Ascription}
 
-\otherform{
-    \nonterm{ E }
-	\quad
-	\exprterminal{to}
-	\quad
-    \nonterm{ T }
-}{Transformation}
-\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
+%\otherform{
+%    \nonterm{ E }
+%	\quad
+%	\exprterminal{to}
+%	\quad
+%    \nonterm{ T }
+%}{Transformation}
+%\otherform{\exprterminal{(} \quad \nonterm{E} \quad \exprterminal{)}}{Parenthesis}
 
 
 $$\\$$
 
 \firstcase{V}{
-    \exprterminal{\epsilon}
-}{Empty Value}
+	\nonterm{ V } \quad
+	\exprterminal{as} \quad
+	\nonterm{ T }
+}{Ascribed Value}
 
 \otherform{
 	\exprterminal{\Lambda} \metavariable{\alpha} \quad
@@ -193,19 +195,14 @@ $$\\$$
 	\nonterm{ E }
 }{Abstraction Value}
 
-\otherform{
-	\nonterm{ V } \quad
-	\exprterminal{as} \quad
-	\nonterm{ T }
-}{Cast Value}
-
 \end{grammar}
 
 
 
 \caption{Syntax of the core calculus with colors for \metavariable{metavariables}, \typeterminal{type-level terminal symbols}, \exprterminal{expression-level terminal symbols}
 where $\typenames, \typevars, \exprvars$ are mutually disjoint, countable sets of symbols to denote atomic type identifiers (\(\typenames\)), typevariables (\(\typevars\)), and expression variables (\(\exprvars\)).
-By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\)
+By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\).
+For simplicity, we write \(\metavariable{e} \in \nonterm{E}\) to say that the term \metavariable{e} is contained in the language generated by the nonterminal \(\nonterm{E}\).
 $$\\$$}
 
 \end{figure}
@@ -242,9 +239,9 @@ The following terms are valid types over \(\Sigma\):
 
 \begin{definition}[Substitution in Types]
 Given a type-variable assignment \(\psi_t = \{ \metavariable{\alpha_1} \mapsto \metavariable{\tau_1}, \quad \metavariable{\alpha_2} \mapsto \metavariable{\tau_2}, \quad \dots \}\),
-the thereby induced, substitution \(\overline{\psi_t}\) replaces all \emph{free} occurences of the variables \(\metavariable{\alpha_i}\) in a type-term \(\metavariable{\xi} \in \typenonterm{\{\metavariable{\alpha_1}, \quad \metavariable{\alpha_2}, \quad \dots\}}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\).
-Occourences of bound variables \(\metavariable{\alpha_i}\) are 
-
+the thereby induced substitution \(\overline{\psi_t}\) replaces all \emph{free} occurences of the variables \(\metavariable{\alpha_i}\) in a type-term \(\metavariable{\xi} \in \nonterm{T}\) recursively with the type-term given by \(\psi_t(\metavariable{\alpha_i})\)
+, while occurences of bound variables are left untouched.
+Further, we assume that for all \(\tau_i\), all variable names are disjunct with the free variables of the term to which the substitution is applied.
 Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
 
 \[\overline{\psi_t} \metavariable{\xi} = \begin{cases}
@@ -261,9 +258,39 @@ Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
 
 \[\overline{\psi_t} \metavariable{e} = \begin{cases}
 \metavariable{e} \quad \text{ if } \metavariable{e} \text{ is a variable}
-\exprterminal{\Lambda \metavariable{\alpha} \mapsto} \overline{\psi_t}\metavariable{e'}  \quad \text{ if \metavariable{e} is of the form } \exprterminal{\Lambda \metavariable{\alpha} \mapsto \metavariable{e'}}\\
-\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto} \overline{\psi_t}\metavariable{e'}  \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto \metavariable{e'}}\\
-\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto_\text{morph}} \overline{\psi_t}\metavariable{e'}  \quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto_\text{morph} \metavariable{e'}}\\
+\\
+
+\exprterminal{\text{let } \metavariable{x} = }\overline{\psi_t}\metavariable{a} \exprterminal{\text{ in }} \overline{\psi_t}\metavariable{e'}
+\quad \text{ if \metavariable{e} is of the form }
+\exprterminal{\text{let } \metavariable{x} = \metavariable{a} \text{ in } \metavariable{e'}}
+\\
+
+\exprterminal{\Lambda \metavariable{\alpha} \mapsto} \overline{\psi_t}\metavariable{e'} 
+\quad \text{ if \metavariable{e} is of the form } \exprterminal{\Lambda \metavariable{\alpha} \mapsto \metavariable{e'}}
+\\
+
+\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto} \overline{\psi_t}\metavariable{e'} 
+\quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto \metavariable{e'}}
+\\
+
+\exprterminal{\lambda \metavariable{x} : }\overline{\psi_t}\metavariable{\tau} \exprterminal{\mapsto_\text{morph}} \overline{\psi_t}\metavariable{e'} 
+\quad \text{ if \metavariable{e} is of the form } \exprterminal{\lambda \metavariable{x} : \metavariable{\tau} \mapsto_\text{morph} \metavariable{e'}}
+\\
+
+\overline{\psi_t} \metavariable{e'} \overline{\psi_t}\metavariable{\tau}
+\quad \text{ if \metavariable{e} is of the form }
+\exprterminal{( \metavariable{e'} \metavariable{\tau} )}
+\\
+
+\overline{\psi_t} \metavariable{e_1} \overline{\psi_t} \metavariable{e_2}
+\quad \text{ if \metavariable{e} is of the form }
+\exprterminal{(\metavariable{e_1} \metavariable{e_2})}
+\\
+
+\overline{\psi_t} \metavariable{e'} \exprterminal{\text{ as }} \overline{\psi_t}\metavariable{\tau}
+\quad \text{ if \metavariable{e} is of the form }
+\exprterminal{ \metavariable{e'} \text{ as } \metavariable{\tau} }
+
 \end{cases}\]
 
 
@@ -276,96 +303,247 @@ Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
 \begin{definition}[Substitution in Expressions]
 \todo{complete}
 Given an expression-variable assignment \(\psi_e = \{ \metavariable{x_1} \mapsto \metavariable{t_1}, \quad \metavariable{x_2} \mapsto \metavariable{t_2}, \quad \dots \}\),
-the thereby induced, lexically scoped substitution \(\overline{\psi_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
-in an expression \(
-	e \in
-	\exprnonterm
-	{\typevars}
-	{\{\metavariable{x_1}, \quad \metavariable{x_2}, \quad \dots\}}
-\). Lexical scoping is implemented by simply not substituting any bound occourences of variables \(\metavariable{\alpha_i}\). This allows to skip \(\alpha\)-conversion as done in classical \(\lambda\)-calculus.
+the thereby induced substitution \(\overline{\psi_e}\) replaces all \emph{free} occurences of the expression variables \(\metavariable{x_i}\)
+in an expression \(e \in \nonterm{E} \) with the \(\psi_e(\metavariable{x_i})\)
+
+\[\overline{\psi_e} \metavariable{e} = \begin{cases}
+
+\metavariable{e} \quad \text{if } \metavariable{e} \in \exprvars \text{ and } \metavariable{e} \notin \text{Dom}(\psi_e)\\
+\metavariable{t} \quad \text{if } \metavariable{e} \in \exprvars \text{ and } (\metavariable{e}\mapsto\metavariable{t}) \in \psi_e\\
+
+\exprterminal{\text{let } \metavariable{x} \text{ = }} \overline{\psi_e}\metavariable{a} \exprterminal{\text{ in }} \overline{\psi_e}\metavariable{e'}
+\quad \text{if }
+\\
+
+\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto }  \overline{\psi_e} \metavariable{e'}
+\quad \text{if \metavariable{e} is of the form }
+\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto \metavariable{e'}}
+\text{ and } \metavariable{x} \notin \text{Dom}(\psi_e)
+\\
+
+\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto }  \overline{\psi_e \setminus \{\metavariable{x} \mapsto \metavariable{t}\}} \metavariable{e'}
+\quad \text{if \metavariable{e} is of the form }
+\exprterminal{\lambda\metavariable{x}:\metavariable{\tau} \mapsto \metavariable{e'}}
+\text{ and } (\metavariable{x}\mapsto\metavariable{t}) \in \psi_e
+\\
+
 
-\[\overline{\psi} \metavariable{e} = \begin{cases}
-\metavariable{e} \quad \text{if } \metavariable{\xi} \in \typenames\\
-\metavariable{\tau} \quad \text{if } (\metavariable{\xi} \mapsto \metavariable{\tau}) \in \psi\\
-\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \overline{\psi}\metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall}  \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \notin \text{Dom}(\psi)\\
-\typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{\forall}  \metavariable{\alpha} \typeterminal{.} \metavariable{\xi'} \text{ and } \metavariable{\alpha} \in \text{Dom}(\psi)\\
-\typeterminal{<} (\overline{\psi} \metavariable{\xi_1}) \quad (\overline{\psi} \metavariable{\xi_2}) \typeterminal{>} \quad \text{if } \metavariable{\xi} \text{ is of the form } \typeterminal{<} \metavariable{\xi_1} \quad \metavariable{\xi_2} \typeterminal{>}\\
-(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow} \metavariable{\xi_2}\\
-(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\rightarrow_{morph}} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\rightarrow_{morph}} \metavariable{\xi_2}\\
-(\overline{\psi} \metavariable{\xi_1}) \typeterminal{\sim} (\overline{\psi} \metavariable{\xi_2}) \quad \text{if } \metavariable{\xi} \text{ is of the form } \metavariable{\xi_1} \typeterminal{\sim} \metavariable{\xi_2}\\
 \end{cases}\]
 
 \end{definition}
 
 \subsection{Typing}
+
 \subsubsection{Equivalence of Type Terms}
 
-\begin{definition}[Distributivity]
-\todo{}
+%We want distributivity of ladders over type-specialization as well as over function/morphism types.
+\begin{definition}[Distributivity in Types]
 
+\begin{mathpar}
+\typeterminal{< \metavariable{\sigma}\sim\metavariable{\sigma'} \quad \metavariable{\tau} >}
+\rightarrow_\text{distribute}
+\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau} > \sim < \metavariable{\sigma'} \quad \metavariable{\tau} > }
+
+\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau}\sim\metavariable{\tau'} >}
+\rightarrow_\text{distribute}
+\typeterminal{< \metavariable{\sigma} \quad \metavariable{\tau} > \sim < \metavariable{\sigma} \quad \metavariable{\tau'} > }
+
+\typeterminal{ \metavariable{\sigma}\sim\metavariable{\sigma'} \rightarrow \metavariable{\tau} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow \metavariable{\tau} ) \sim ( \metavariable{\sigma'} \rightarrow \metavariable{\tau} ) }
+
+\typeterminal{ \metavariable{\sigma} \rightarrow \metavariable{\tau}\sim\metavariable{\tau'} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow \metavariable{\tau} ) \sim ( \metavariable{\sigma} \rightarrow \metavariable{\tau'} ) }
+
+\typeterminal{ \metavariable{\sigma}\sim\metavariable{\sigma'} \rightarrow_\text{morph} \metavariable{\tau} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau} ) \sim ( \metavariable{\sigma'} \rightarrow_\text{morph} \metavariable{\tau} ) }
+
+\typeterminal{ \metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau}\sim\metavariable{\tau'} }
+\rightarrow_\text{distribute}
+\typeterminal{ (\metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau} ) \sim ( \metavariable{\sigma} \rightarrow_\text{morph} \metavariable{\tau'} ) }
+
+\end{mathpar}
+
+
+Let \(\rightarrow_\text{condense}\) be the inverse to \(\rightarrow_\text{distribute}\).
 
 See \hyperref[coq:type-dist]{equiv.v:\ref{coq:type-dist}}.
 \end{definition}
 
-\begin{definition}[Equivalence Relation]
-\todo{}
+\begin{definition}[Alpha Conversion in Types]
+\begin{mathpar}
+\typeterminal{\forall \metavariable{\alpha} . \metavariable{\tau}}
+\rightarrow_{\alpha}
+\typeterminal{\forall \metavariable{\alpha'} . } \{ \metavariable{\alpha} \mapsto \metavariable{\alpha'} \} \metavariable{\tau}
 
+\end{mathpar}
+\end{definition}
+
+\begin{definition}[Equivalence Relation]
+Transitive closure over \(\rightarrow_\text{distribute}\), \(\rightarrow_\text{condense}\) and \(\rightarrow_\alpha\).
+
+
+\begin{mathpar}
+
+\inferrule[E-Refl]{
+	\metavariable{\tau} \in \nonterm{T}
+}{
+	\metavariable{\tau} \equiv \metavariable{\tau}
+}\and
+\inferrule[E-Trans]{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}\\
+	\metavariable{\tau_2} \equiv \metavariable{\tau_3}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_3}
+}
+
+\inferrule[E-Rename]{
+	\metavariable{\tau_1} \rightarrow_\alpha \metavariable{\tau_2}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}
+
+\inferrule[E-Distribute]{
+	\metavariable{\tau_1} \rightarrow_\text{distribute} \metavariable{\tau_2}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}\and
+\inferrule[E-Condense]{
+	\metavariable{\tau_1} \rightarrow_\text{condense} \metavariable{\tau_2}
+}{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}
+
+\end{mathpar}
 
 See \hyperref[coq:type-equiv]{equiv.v:\ref{coq:type-equiv}}.
 \end{definition}
 
+
+\begin{lemma}[Symmetry of \(\equiv\)]
+
+\begin{mathpar}
+\inferrule[E-Symm]{
+	\metavariable{\tau_1} \equiv \metavariable{\tau_2}
+}{
+	\metavariable{\tau_2} \equiv \metavariable{\tau_1}
+}
+\end{mathpar}
+
+\begin{proof}
+\(\rightarrow_{distribute}\) is the inverse of \(\rightarrow_{condense}\) and \(\rightarrow_{\alpha}\) is symmetric by itself.
+\end{proof}
+
+\end{lemma}
+
 \subsubsection{Normal Forms}
 
 \begin{definition}[Ladder Normal Form]
-\todo{}
+LNF is reached by exhaustive application of \(\rightarrow_\text{distribute}\).
 \end{definition}
 
-\subsubsection{Subtyping}
-
-\begin{definition}[Syntactic Subtyping]
-\todo{}
+\begin{definition}[Parameter Normal Form]
+PNF reached by exhaustive application of \(\rightarrow_\text{condense}\).
 \end{definition}
 
-\begin{definition}[Semantic Subtyping]
-\todo{}
+\subsubsection{Subtype Relations}
+
+We define two relations: first the syntatic subtype relation \(\leq\) and second the semantic subtype relation \(\precsim\).
+
+\begin{definition}[Syntactic Subtype (\(\tau_1\leq\tau_2\))]
+\begin{mathpar}
+\inferrule[S-Refl]{	
+	\metavariable{\tau} \equiv \metavariable{\tau'}
+}{
+	\metavariable{\tau} \leq \metavariable{\tau'}
+}
+
+\inferrule[S-Syntactic]{
+	\metavariable{\sigma} \leq \metavariable{\tau}
+}{
+	\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \leq \metavariable{\tau}
+}
+\end{mathpar}
 \end{definition}
 
+\begin{definition}[Semantic Subtype (\(\tau_1\precsim\tau_2\))]
+\begin{mathpar}
+
+\inferrule[S-Refl]{	
+	\metavariable{\tau} \equiv \metavariable{\tau'}
+}{
+	\metavariable{\tau} \precsim \metavariable{\tau'}
+}
+
+\inferrule[S-Syntactic]{
+	\metavariable{\sigma} \precsim \metavariable{\tau}
+}{
+	\metavariable{\sigma'} \typeterminal{\sim} \metavariable{\sigma} \precsim \metavariable{\tau}
+}
+
+\inferrule[S-Semantic]{
+	\metavariable{\sigma} \equiv \metavariable{\tau}
+}{
+	\metavariable{\sigma} \typeterminal{\sim} \metavariable{\sigma'} \precsim \metavariable{\tau} \typeterminal{\sim} \metavariable{\tau'}
+}
+
+
+\end{mathpar}
+\end{definition}
+
+
+\begin{example}[Syntactic \& Semantic Subtypes]$\\$
+
+\begin{enumerate}
+\item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \leq \quad \) Char }\\
+.. is a \emph{syntactic subtype}, because the representation of \typeterminal{<Digit 10>} is \emph{embedded} into \typeterminal{Char}.\\
+
+\item \typeterminal{ <Digit 10> \(\sim\) Char \( \quad \precsim \quad \) <Digit 10> \(\sim\) machine.UInt64}\\
+.. is a \emph{semantic subtype}, because the \typeterminal{Char} based representation can be transformed into a representation based on \typeterminal{machine.UInt64},
+while preserving its semantics.
+\end{enumerate}
+\end{example}
+
 \subsubsection{Inference of Expression Types}
 
-The type-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\) is a finite mapping from variables \(\metavariable{x_i} \in \exprvars\) to ground types \(\metavariable{\tau_i} \in \typenonterm{\emptyset}\).
+As usual, the typing-context \(\Gamma = \{ \metavariable{x_1} : \metavariable{\tau_1} , \quad \metavariable{x_2} : \metavariable{\tau_2} , \quad \ldots \}\)
+is a finite mapping which assigns variables \(\metavariable{x_i} \in \exprvars\) to types \(\metavariable{\tau_i} \in \nonterm{T}\).
 Using the inference rules given in \ref{def:typerules}, further typing-judgements
 of the form
 \begin{itemize}
-\item \(\metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
-\item \(\metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
+\item \(\Gamma \vdash \metavariable{e} : \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is of type \(\metavariable{\tau}\)" and
+\item \(\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau} \quad\) read as "expression \(\metavariable{e}\) is compatible with type \(\metavariable{\tau}\)"
 \end{itemize}
-can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \exprnonterm{\emptyset}{\exprvars}\) and \(\metavariable{\tau} \in \typenonterm{\emptyset}\)
+can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
+
+
 
 \begin{definition}[Syntactic Well-Typedness]
-An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
 such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
 \end{definition}
 
 \begin{definition}[Semantic Well-Typedness]
-An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
-such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules}.
+An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{semantically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
+such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) by \ref{def:typerules} and \ref{def:semtyperules}.
 \end{definition}
 
-\begin{definition}[Inference Rules for the Typing Relation.]
-  \label{def:typerules}
 
-As usual, each rule is composed of premises (above the horizontal line) and a conclusion (below the line):
+\begin{definition}[Syntactic Typing Relation]
+
+\label{def:typerules}
 \begin{mathpar}
 
 	\inferrule[T-Variable]{
-		\metavariable{x} \in \exprvars\\
-		\metavariable{\tau} \in \nonterm{T}\\
+%		\metavariable{x} \in \exprvars\\
+%		\metavariable{\tau} \in \nonterm{T}\\
 		\metavariable{x}:\metavariable{\tau} \in \Gamma\\
 	}{
 		\Gamma \vdash \metavariable{x}:\metavariable{\tau}
 	}\and
 
-
 	\inferrule[T-LetBinding]{
 		\Gamma \vdash \metavariable{e} : \metavariable{\sigma} \\
 		\Gamma , \metavariable{x}:\metavariable{\sigma} \vdash \metavariable{t} : \metavariable{\tau}
@@ -373,17 +551,16 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
 		\Gamma \vdash (\exprterminal{\text{let }}\metavariable{x}\exprterminal{\text{ = }}\metavariable{e}\exprterminal{\text{ in }} \metavariable{t}) : \metavariable{\tau}
 	}
 
-
 	\inferrule[T-TypeAbs]{
-		\metavariable{\tau} \in \nonterm{T} \\
-		\metavariable{e} \in \nonterm{E} \\
+%		\metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{e} \in \nonterm{E} \\
 		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
 	}{
         \Gamma \vdash (\exprterminal{\Lambda} \metavariable{\alpha} \exprterminal{\mapsto} \metavariable{e}) : \typeterminal{\forall}\metavariable{\alpha}\typeterminal{.}\metavariable{\tau}
 	}
 
 	\inferrule[T-TypeApp]{
-		\metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{\tau} \in \nonterm{T} \\
 		\Gamma \vdash \metavariable{e} : \typeterminal{\forall} \metavariable{\alpha} \typeterminal{.} \metavariable{\tau} \\
 		\metavariable{\sigma} \in \nonterm{T}
 	}{
@@ -391,42 +568,34 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
 	}
 
 
-	\inferrule[T-ValueAbs]{
-		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
-		\metavariable{e} \in \nonterm{E} \\
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
+	\inferrule[T-Abs]{
+%		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{e} \in \nonterm{E} \\
+		\Gamma,\metavariable{x}:\metavariable{\sigma} \vdash \metavariable{e} : \metavariable{\tau} \\
 	}{
         \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
 	}
 
-	\inferrule[T-ValueApp]{
+	\inferrule[T-App]{
 		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
 		\Gamma \vdash \metavariable{a} : \metavariable{\sigma} \\
 	}{
 		\Gamma \vdash (\metavariable{f} \quad \metavariable{a}) : \metavariable{\tau}
 	}\and
 
-
-	\inferrule[T-Compatible]{
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau}
-	}{
-		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}
-	}\and
-	
 	\inferrule[T-MorphAbs]{
-		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
-		\metavariable{e} \in \nonterm{E} \\
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau} \\
-	}{
-        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
-	}\and
-
-	\inferrule[T-MorphApp]{
-		\Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
-		\exists \metavariable{h} . \Gamma \vdash \metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_{morph}} \metavariable{\tau'}\\
+%		\metavariable{\sigma}, \metavariable{\tau} \in \nonterm{T} \\
+%		\metavariable{e} \in \nonterm{E} \\
+		\Gamma,\metavariable{x}:\metavariable{\tau} \vdash \metavariable{e} : \metavariable{\tau'} \\
 		\metavariable{\tau} \precsim \metavariable{\tau'}
 	}{
-		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
+        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_{morph}}\metavariable{\tau'}
+	}\and
+
+	\inferrule[T-MorphFun]{
+        \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
+	}{
+        \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
 	}\and
 
 	\inferrule[T-Ascension]{
@@ -441,16 +610,98 @@ As usual, each rule is composed of premises (above the horizontal line) and a co
 		\metavariable{\tau} \leq \metavariable{\tau'}
 	}{
 		\Gamma \vdash \metavariable{e} : \metavariable{\tau'}
-	}\and
+	}
 
 \end{mathpar}
 \end{definition}
 
+\begin{definition}[Semantic Typing Relation]
+\label{def:semtyperules}
+\begin{mathpar}
+	\inferrule[T-NativeRepr]{
+		\Gamma\vdash \metavariable{e} : \metavariable{\tau}
+	}{
+		\Gamma\vdash \metavariable{e} :\approx \metavariable{\tau}
+	}
+
+	\inferrule[T-CoercedRepr]{
+		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau}\\
+%		\metavariable{\tau} \precsim \metavariable{\tau'}\\
+		%\exists \metavariable{h} \text{ s.t. }
+		\Gamma \vdash \metavariable{h}: \typeterminal{\metavariable{\tau}\rightarrow_\text{morph}\metavariable{\tau'}}
+	}{
+		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
+	}
+
+
+	\inferrule[T-CompatibleApp]{
+		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \rightarrow \metavariable{\tau}\\
+		\Gamma \vdash \metavariable{a} :\approx \metavariable{\sigma}
+	}{
+		\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
+	}
+\end{mathpar}
+\end{definition}
+
+\subsection{Coercion Semantics}
+
+We define the translation function \(\llbracket . \rrbracket\) which completes a \emph{semantically well-typed} expression
+by inserting all required coercions based on the typing derivation of the expression.
+The result shall be a \emph{syntactically well-typed} expression.
+
+We write \(C :: \sigma \precsim \tau\) to mean "C is a subtyping derivation tree whose conclusion is \(\sigma \precsim \tau\)".
+Similarly, we write \(D :: \Gamma \vdash e : \tau\) to mean "D is a typing derivation whose conclusion is \(\Gamma \vdash e : \tau\)"
+
+\begin{definition}[Translation]
+\begin{mathpar}
+
+\Big{\llbracket} \inferrule[T-SemanticSubtype]{
+	D_1 :: \Gamma \vdash \metavariable{h}:\metavariable{\tau} \typeterminal{\rightarrow_\text{morph}} \metavariable{\tau'}\\
+    D_2 :: \Gamma \vdash \metavariable{e}:\metavariable{\tau}\\
+%	C :: \metavariable{\tau} \precsim \metavariable{\tau'}
+}{
+	\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
+}\Big{\rrbracket} = \exprterminal{(}
+\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
+%\metavariable{h} \llbracket D_2 \rrbracket
+\exprterminal{)}
+
+\Big{\llbracket} \inferrule[T-CoercedApp]{
+	D_1 :: \Gamma \vdash \metavariable{f}:\metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau}\\
+    D_2 :: \Gamma \vdash \metavariable{a}:\approx\metavariable{\sigma}
+}{
+	\Gamma \vdash \exprterminal{(\metavariable{f} \text{ } \metavariable{a})} : \metavariable{\tau}
+}\Big{\rrbracket} = \exprterminal{(}
+%\exprterminal{(}\metavariable{f} \llbracket D_2 \rrbracket \exprterminal{)}
+\llbracket D_1 \rrbracket \llbracket D_2 \rrbracket
+\exprterminal{)}
+
+\Big{\llbracket}
+\inferrule[\emph{Otherwise}]{}{
+D :: \Gamma \vdash \metavariable{e} : \metavariable{\tau}
+}
+\Big{\rrbracket} = \metavariable{e}
+
+\end{mathpar}
+\end{definition}
+
+\begin{lemma}[Elimination of \(:\approx\)]
+\label{lemma:translation}
+
+For all \emph{semantically well-typed} expressions \metavariable{e} with the typing derivation \(D :: \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\),
+the translation \(\llbracket D \rrbracket = \metavariable{e'}\), yields a \emph{syntactically well-typed} expression \metavariable{e'} with
+\(\emptyset \vdash \metavariable{e'} : \metavariable{\tau} \)
+
+\begin{proof}
+\todo{}
+\end{proof}
+
+\end{lemma}
+
 
 \subsection{Evaluation}
 
-Evaluation of an expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is defined by exhaustive application of the rewrite rules \(\rightarrow_\beta\) and \(\rightarrow_\delta\),
-which are given in \ref{def:evalrules}.
+Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by exhaustive application of the rewrite rule \(\rightarrow_\beta\) as in \ref{def:evalrules}.
 
 \begin{definition}[Inference Rules for Evaluation]
 \label{def:evalrules}
@@ -468,13 +719,13 @@ which are given in \ref{def:evalrules}.
 	\inferrule[E-App2]{
 		\metavariable{e_2} \rightarrow_\beta \metavariable{e_2'}
 	}{
-		\metavariable{e_1} \metavariable{e_2}
+		\metavariable{v_1} \metavariable{e_2}
 		\rightarrow_\beta
-		\metavariable{e_1} \metavariable{e_2'}
-	}
+		\metavariable{v_1} \metavariable{e_2'}
+	}\and
 
 	\inferrule[E-TypApp]{
-		\metavariable{\tau} \in \typenonterm{\emptyset}\\
+%		\metavariable{\tau} \in \typenonterm{\emptyset}\\
 		\metavariable{e} \rightarrow_\beta \metavariable{e'}
 	}{
 		\metavariable{e}
@@ -495,7 +746,6 @@ which are given in \ref{def:evalrules}.
 		\rightarrow_\beta
 		\{ \metavariable{\alpha} \mapsto \metavariable{\tau} \} \metavariable{e}
 	}\and
-
 	\inferrule[E-AppLam]{
 	}{
 		\exprterminal{(\lambda} \metavariable{x}
@@ -514,64 +764,27 @@ which are given in \ref{def:evalrules}.
 		\exprterminal{\text{ in }}\metavariable{e}
 		\rightarrow_\beta
 		\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
-	}
-
-
-	\inferrule[E-ImplicitCast]{
-		\Gamma \vdash \metavariable{f} : \metavariable{\sigma} \typeterminal{\rightarrow} \metavariable{\tau} \\
-		\Gamma \vdash \metavariable{h} : \metavariable{\sigma'} \typeterminal{\rightarrow_{morph}} \metavariable{\sigma} \\
-		\Gamma \vdash \metavariable{a} : \metavariable{\sigma'}
+	}\and
+	\inferrule[E-Ascribe]{
 	}{
-		\exprterminal{(} \metavariable{f} \quad \metavariable{a} \exprterminal{)}
-		\rightarrow_\delta
-		\exprterminal{(} \metavariable{f} \quad \exprterminal{(} \metavariable{h} \quad \metavariable{a} \exprterminal{))}
+		\metavariable{e}
+		\exprterminal{\text{ as }}
+		\metavariable{\tau}
+		\rightarrow_\beta
+		\metavariable{e}
 	}
-
 \end{mathpar}
 \end{definition}
 
 
-\begin{lemma}[\(\beta\)-reduction preserves \(\delta\)-normalform]
-\label{lemma:preserve-delta-normalform}
-Assume \metavariable{e} is in \(\delta\)-normalform and \(\metavariable{e} \rightarrow_\beta \metavariable{e'}\). Then \(\metavariable{e'}\) is in \(\delta\)-normalform as well.
-\begin{proof}
-\todo{}
-\end{proof}
-\end{lemma}
-
-\begin{lemma}[\(\delta\)-normalform eliminates compatibility]
-\label{lemma:eliminate-compat}
-Assume \(\emptyset \vdash \metavariable{e} :\approx \metavariable{\tau}\) and \(\metavariable{e} \rightarrow_{\delta}^* \metavariable{e'}\) such that \(\metavariable{e'}\) is in \(\delta\)-normalform.
-Then \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) 
-
-\begin{proof}
-\end{proof}
-
-\end{lemma}
-
 \subsection{Soundness}
 
-\begin{lemma}[\(\beta\)-Preservation]
-\label{lemma:beta-preservation}
-Assume the expression \(\metavariable{e}\) is \textbf{syntactically well-typed}, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
-
-\begin{proof}
-\todo{}
-\end{proof}
-
-\end{lemma}
-
-\begin{lemma}[\(\delta\)-Preservation]
-\label{lemma:delta-preservation}
-
-\begin{proof}
-\todo{}
-\end{proof}
-\end{lemma}
-
 \begin{lemma}[Preservation]
 \label{lemma:preservation}
-Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\) for some type \(\metavariable{\tau}\). Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
+Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\)
+for some type \(\metavariable{\tau}\).
+Then forall \(\metavariable{e'}\) with \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
+it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
 
 \begin{proof}
 \todo{}
@@ -580,23 +793,44 @@ Assume the expression \(\metavariable{e}\) is well typed, i.e. \(\emptyset \vdas
 
 \begin{lemma}[Progress]
 \label{lemma:progress}
-If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\), then either \(\metavariable{e}\) is a value or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{eval} \metavariable{e'}\)
+If \(\emptyset \vdash \metavariable{e} : \metavariable{\tau}\),
+then either \(\metavariable{e}\) is a value
+or there exists some \(\metavariable{e'}\) such that \(\metavariable{e} \rightarrow_{\beta} \metavariable{e'}\)
 
 \begin{proof}
 \todo{}
 \end{proof}
 \end{lemma}
 
-\begin{theorem}[Soundness]
-If \(\emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\), then it never occurs that \(\metavariable{e} \rightarrow_{eval}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
+\begin{theorem}[Syntactic Type Soundness]
+\label{theorem:syntactic-soundness}
+No syntactically well-typed expression is stuck.
+
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\metavariable{\tau}\).
+Then it never occurs that \(\metavariable{e} \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
 
 \begin{proof}
-By \ref{lemma:}
 Follows from \ref{lemma:progress} and \ref{lemma:preservation}.
 \end{proof}
 \end{theorem}
 
+\begin{theorem}[Semantic Type Soundness]
+\label{theorem:semantic-soundness}
+No semantically well-typed expression is stuck.
 
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
+Then it never occurs that \(\llbracket D \rrbracket \rightarrow_{\beta}^{*} \metavariable{e'}\) where \metavariable{e'} is in normal form but not a value.
+
+\begin{proof}
+Assume the typing derivation \(D :: \emptyset \vdash \metavariable{e}:\approx\metavariable{\tau}\).
+By \ref{lemma:translation}, \(\emptyset \vdash \llbracket D \rrbracket : \metavariable{\tau}\)
+and thus it follows by \ref{theorem:syntactic-soundness} that \metavariable{e} is not stuck.
+\end{proof}
+\end{theorem}
+
+
+
+\newpage
 \section{Boehm-Berarducci Encoding}