paper/main.tex

@@ -116,13 +116,6 @@ $$\\$$
 	{ \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 $$
@@ -143,6 +136,13 @@ $$\\$$
 	\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,25 +161,23 @@ $$\\$$
 	\exprterminal{as}
 	\quad
     \nonterm{ T }
-}{Ascription}
+}{Up-Cast}
 
-%\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}{
-	\nonterm{ V } \quad
-	\exprterminal{as} \quad
-	\nonterm{ T }
-}{Ascribed Value}
+    \exprterminal{\epsilon}
+}{Empty Value}
 
 \otherform{
 	\exprterminal{\Lambda} \metavariable{\alpha} \quad
@@ -195,14 +193,19 @@ $$\\$$
 	\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\).
-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}\).
+By default, assume \(\metavariable{\sigma} \in \typenames\), \(\metavariable{\alpha} \in \typevars\) and \(\metavariable{x} \in \exprvars\)
 $$\\$$}
 
 \end{figure}
@@ -239,9 +242,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 \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.
+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 
+
 Coq definition is at \hyperref[coq:subst-type]{subst.v:\ref{coq:subst-type}}.
 
 \[\overline{\psi_t} \metavariable{\xi} = \begin{cases}
@@ -258,39 +261,9 @@ 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{\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} }
-
+\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'}}\\
 \end{cases}\]
 
 
@@ -303,247 +276,96 @@ 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 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
-\\
-
+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.
 
+\[\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}
 
-%We want distributivity of ladders over type-specialization as well as over function/morphism types.
-\begin{definition}[Distributivity in Types]
+\begin{definition}[Distributivity]
+\todo{}
 
-\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}[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\).
+\todo{}
 
 
-\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]
-LNF is reached by exhaustive application of \(\rightarrow_\text{distribute}\).
+\todo{}
 \end{definition}
 
-\begin{definition}[Parameter Normal Form]
-PNF reached by exhaustive application of \(\rightarrow_\text{condense}\).
+\subsubsection{Subtyping}
+
+\begin{definition}[Syntactic Subtyping]
+\todo{}
 \end{definition}
 
-\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}
+\begin{definition}[Semantic Subtyping]
+\todo{}
 \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}
 
-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}\).
+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}\).
 Using the inference rules given in \ref{def:typerules}, further typing-judgements
 of the form
 \begin{itemize}
-\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}\)"
+\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}\)"
 \end{itemize}
-can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \nonterm{E}\) and \(\metavariable{\tau} \in \nonterm{T}\).
-
-
+can be derived from the context \(\Gamma\) where \(\metavariable{e} \in \exprnonterm{\emptyset}{\exprvars}\) and \(\metavariable{\tau} \in \typenonterm{\emptyset}\)
 
 \begin{definition}[Syntactic Well-Typedness]
-An expression \(\metavariable{e} \in \nonterm{E}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \nonterm{T}\),
+An expression \(\metavariable{e} \in \exprnonterm{\emptyset}{\emptyset}\) is \textbf{syntactically well-typed} if there exists a type \(\metavariable{\tau} \in \typenonterm{\emptyset}\),
 such that \( \emptyset \vdash \metavariable{e} : \metavariable{\tau} \) by \ref{def:typerules}.
 \end{definition}
 
 \begin{definition}[Semantic Well-Typedness]
-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}.
+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}.
 \end{definition}
 
+\begin{definition}[Inference Rules for the Typing Relation.]
+  \label{def:typerules}
 
-\begin{definition}[Syntactic Typing Relation]
-
-\label{def:typerules}
+As usual, each rule is composed of premises (above the horizontal line) and a conclusion (below the line):
 \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}
@@ -551,16 +373,17 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b
 		\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}
 	}{
@@ -568,34 +391,42 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b
 	}
 
 
-	\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} \\
+	\inferrule[T-ValueAbs]{
+		\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{\sigma} \exprterminal{\mapsto} \metavariable{e}) : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
 	}
 
-	\inferrule[T-App]{
+	\inferrule[T-ValueApp]{
 		\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-MorphAbs]{
-%		\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'}
+
+	\inferrule[T-Compatible]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau}
 	}{
-        \Gamma \vdash (\exprterminal{\lambda} \metavariable{x} \exprterminal{:} \metavariable{\tau} \exprterminal{\mapsto_{morph}} \metavariable{e}) : \metavariable{\tau}\typeterminal{\rightarrow_{morph}}\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-MorphFun]{
-        \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow_{morph}}\metavariable{\tau}
+	\inferrule[T-MorphApp]{
+		\Gamma \vdash \metavariable{e} : \metavariable{\tau}\\
+		\exists \metavariable{h} . \Gamma \vdash \metavariable{h} : \metavariable{\tau} \typeterminal{\rightarrow_{morph}} \metavariable{\tau'}\\
+		\metavariable{\tau} \precsim \metavariable{\tau'}
 	}{
-        \Gamma \vdash \metavariable{f} : \metavariable{\sigma}\typeterminal{\rightarrow}\metavariable{\tau}
+		\Gamma \vdash \metavariable{e} :\approx \metavariable{\tau'}
 	}\and
 
 	\inferrule[T-Ascension]{
@@ -610,98 +441,16 @@ such that \( \emptyset \vdash \metavariable{e} :\approx \metavariable{\tau} \) b
 		\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 \nonterm{E}\) is defined by exhaustive application of the rewrite rule \(\rightarrow_\beta\) as in \ref{def:evalrules}.
+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}.
 
 \begin{definition}[Inference Rules for Evaluation]
 \label{def:evalrules}
@@ -719,13 +468,13 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
 	\inferrule[E-App2]{
 		\metavariable{e_2} \rightarrow_\beta \metavariable{e_2'}
 	}{
-		\metavariable{v_1} \metavariable{e_2}
+		\metavariable{e_1} \metavariable{e_2}
 		\rightarrow_\beta
-		\metavariable{v_1} \metavariable{e_2'}
-	}\and
+		\metavariable{e_1} \metavariable{e_2'}
+	}
 
 	\inferrule[E-TypApp]{
-%		\metavariable{\tau} \in \typenonterm{\emptyset}\\
+		\metavariable{\tau} \in \typenonterm{\emptyset}\\
 		\metavariable{e} \rightarrow_\beta \metavariable{e'}
 	}{
 		\metavariable{e}
@@ -746,6 +495,7 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
 		\rightarrow_\beta
 		\{ \metavariable{\alpha} \mapsto \metavariable{\tau} \} \metavariable{e}
 	}\and
+
 	\inferrule[E-AppLam]{
 	}{
 		\exprterminal{(\lambda} \metavariable{x}
@@ -764,27 +514,64 @@ Evaluation of an expression \(\metavariable{e} \in \nonterm{E}\) is defined by e
 		\exprterminal{\text{ in }}\metavariable{e}
 		\rightarrow_\beta
 		\{ \metavariable{x} \mapsto \metavariable{a} \} \metavariable{e}
-	}\and
-	\inferrule[E-Ascribe]{
-	}{
-		\metavariable{e}
-		\exprterminal{\text{ as }}
-		\metavariable{\tau}
-		\rightarrow_\beta
-		\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'}
+	}{
+		\exprterminal{(} \metavariable{f} \quad \metavariable{a} \exprterminal{)}
+		\rightarrow_\delta
+		\exprterminal{(} \metavariable{f} \quad \exprterminal{(} \metavariable{h} \quad \metavariable{a} \exprterminal{))}
+	}
+
 \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_{\beta} \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_{eval} \metavariable{e'}\) it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as well.
 
 \begin{proof}
 \todo{}
@@ -793,44 +580,23 @@ it holds that \(\emptyset \vdash \metavariable{e'} : \metavariable{\tau}\) as we
 
 \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_{\beta} \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_{eval} \metavariable{e'}\)
 
 \begin{proof}
 \todo{}
 \end{proof}
 \end{lemma}
 
-\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{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{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}