1. All we we would need to add to the syntax is the expression:
   Let *Ident*=*Expr* in *Expr*
   We will now extend the the static semantics as follows:
   $$\frac{\Gamma \vdash e_1:\tau_1\ \ \ \Gamma\cup \{x:\tau_1\} \vdash e_2 : \tau}{\Gamma \vdash\text{Let } x=e_1\text{ in } e_2:\tau}$$
   **How would the static semantics rule change if we extend the scope of the bound variable to the right handside of the binding (like in Haskell)?**
   $$\frac{\Gamma\cup \{x:\tau_1\} \vdash e_1:\tau_1\ \ \ \Gamma\cup \{x:\tau_1\} \vdash e_2 : \tau}{\Gamma \vdash\text{Let } x=e_1\text{ in } e_2:\tau}$$
   With the second rule it works, because it is now able to access f and earlier it was not
2. **Progress.** Assume that we can derive $\vdash e : \tau$. If $e$ is in a final state we are done, so we will assume that $e$ is not in a final state. We will now go through all possible non-final states.
   - *Binary operations:* 
     Assumption: We can derive $\Gamma \vdash e_1 : \tau_1$ and $\Gamma \vdash e_2 : \tau_2$
     IH: $e_1$ is either a final state or there is a $e_1'$ such that $e_1\mapsto e_1'$. The same holds for $e_2$.
     
     If there exists a $e_1'$ such that $e_1\mapsto e_1'$ then we see that $$\text{Operation-}\otimes e_1 e_2 \mapsto \text{Operation-}\otimes e_1' e_2$$
     If $e_1$ is in it's final state and there exists a $e_2'$ such that $e_2\mapsto e_2'$ we see that$$\text{Operation-}\otimes e_1 e_2 \mapsto \text{Operation-}\otimes e_1 e_2'$$
     If $e_1$ and $e_2$ are both in their final state then we see that $e_1 = \text{Const-}\tau_1 v_1$ and $e_2 = \text{Const-}\tau_2v_2$, so
     $$\text{Operation-}\otimes e_1 e_2 \mapsto \text{Const-}\tau (v_1\otimes v_2) $$
   - *Conditionals:*
     Assumption: We can derive $\Gamma \vdash e_1 : \text{Bool}$, $\Gamma \vdash e_2 : \tau$, $\Gamma \vdash e_3:\tau$
     IH: $e_1$ is either a final state or there is a $e_1'$ such that $e\mapsto e_1'$.
     
     If there exists a $e_1'$ such that $e_1\mapsto e_1'$ we see that $$\text{If }e_1\text{ Then }e_2 \text{ Else } e_3 \mapsto \text{If }e_1'\text{ Then }e_2 \text{ Else } e_3$$ If $e_1$ is in a final state we know that $e_1 = \text{Const} \text{ True}$ or $e_1 = \text{Const} \text{ False}$. We see that $$\text{If }e_1\text{ Then }e_2 \text{ Else } e_3 \mapsto e_2$$ or $$\text{If }e_1\text{ Then }e_2 \text{ Else } e_3 \mapsto e_3$$ respectively.
   - *Application:*
     Assumption: $\Gamma \vdash e_1: \tau_1\to \tau_2$ and $\Gamma \vdash e_2 : \tau_1$
     IH: $e_1$ is either a final state or there is a $e_1'$ such that $e_1\mapsto e_1'$. The same holds for $e_2$.
     
     If there exists a $e_1'$ such that $e_1 \mapsto e_1'$ we see that $$\text{Apply } e_1 e_2 \mapsto \text{Apply } e_1' e_2.$$ If $e_1$ is a final state and there exists $e_2'$ such that $e_2\mapsto e_2'$ then 
     $$\text{Apply } e_1 e_2 \mapsto \text{Apply } e_1 e_2'.$$
	    If $e_1$ and $e_2$ are in a final state we see that $e_1= \text{Recfun } \tau_1 \tau_2 (f.(x.e))$, so
	    $$\text{Apply } e_1 e_2 \mapsto e_2[f:=e_1][x:=e_2].$$
	**Preservation:** For $e\mapsto e'$ we have the following cases.
	- *Binary operation:* 
	  Assumption: We can derive $\vdash e_1:\tau_1$ and $\vdash e_2 : \tau_2$
	  IH: If $e_1\mapsto e_1'$ then $\vdash e_1' : \tau_1$ can be derived. The same for $e_2$.
	  
	  Given an operator $\otimes:\tau_1\to \tau_2 \to \tau_3 $. We see that $\vdash\text{Operator-}\otimes e_1 e_2:\tau_3$
	  If $e_1$ is not in a final state we know from earlier that there exists a $e_1'$ such that $e_1\mapsto e_1'$. We know from the IH that $\vdash e_1': \tau_1$ , so $$\text{Operator-}\otimes e_1 e_2\mapsto \text{Operator-}\otimes e_1' e_2$$
	  and $\vdash \text{Operator-}\otimes e_1' e_2 : \tau_2$.  If $e_2$ is not in a final state we know from earlier that there exists a $e_2'$ such that $e_2\mapsto e_2'$. We know from the IH that $\vdash e_2': \tau_1$ , so $$\text{Operator-}\otimes e_1 e_2\mapsto \text{Operator-}\otimes e_1 e_2'$$
	  and $\vdash \text{Operator-}\otimes e_1 e_2' : \tau_2$. 
	  If $e_1$ and $e_2$ are in a final state we know that $e_1 = \text{Const-}\tau_1 v_1$ and $e_2 = \text{Const-}\tau_2v_2$, so $$\text{Operation-}\otimes e_1 e_2 \mapsto \text{Const-}\tau_3 (v_1\otimes v_2) $$ and we see that $\vdash \text{Const-}\tau_3 (v_1\otimes v_2) : \tau_3$
	- *Conditionals:* 
	  Assumption: We can derive $\Gamma \vdash e_1 : \text{Bool}$, $\Gamma \vdash e_2 : \tau$, $\Gamma \vdash e_3:\tau$
      IH: If $e_1\mapsto e_1'$ then $e_1':\text{Bool}$.
      
      We see that $\vdash \text{If }e_1\text{ Then } e_2 \text{ Else } e_3:\tau$. If $e_1$ is not in a final state there exists $e_1'$ such that $e_1\mapsto e_1'$, so $$\text{If }e_1\text{ Then }e_2 \text{ Else } e_3 \mapsto \text{If }e_1'\text{ Then }e_2 \text{ Else } e_3.$$ And we see that $e_1':\text{Bool}$, so $\text{If }e_1'\text{ Then }e_2 \text{ Else } e_3:\tau$. If $e_1$ is in a final state we know that $e_1 = \text{Const} \text{ True}$ or $e_1 = \text{Const} \text{ False}$. We see that $$\text{If }e_1\text{ Then }e_2 \text{ Else } e_3 \mapsto e_2$$ or $$\text{If }e_1\text{ Then }e_2 \text{ Else } e_3 \mapsto e_3$$ respectively. We know  that $e_2:\tau$ and $e_3:\tau$.
    - *Application* 
      Assumption: $\Gamma \vdash e_1: \tau_1\to \tau_2$ and $\Gamma \vdash e_2 : \tau_1$
     IH: If $e_1\mapsto e_1'$ then $\vdash e_1' : \tau_1\to \tau_2$ can be derived. If $e_1\mapsto e_2'$ then $\vdash e_2' : \tau_2$.
		
     We see that $\vdash \text{Apply }e_1e_2 : \tau_2$. If there exists a $e_1'$ such that $e_1 \mapsto e_1'$ we see that $$\text{Apply } e_1 e_2 \mapsto \text{Apply } e_1' e_2.$$Because of IH we know that $\vdash e_1:\tau_1\to \tau_2$, so $\vdash \text{Apply }e_1e_2 : \tau_2$.  If $e_2$ is a final state and there exists $e_2'$ such that $e_2\mapsto e_2'$ then 
     $$\text{Apply } e_1 e_2 \mapsto \text{Apply } e_1 e_2'.$$
	    Because of IH we see that $e_2' : \tau_1$, so $\text{Apply } e_1 e_2':\tau_2$. If $e_1$ and $e_2$ are in a final state we see that $e_1= \text{Recfun } \tau_1 \tau_2 (f.(x.e))$ where $e:\tau_2$ so
	    $$\text{Apply } e_1 e_2 \mapsto e[f:=e_1][x:=e_2]$$ and $e[f:=e_1][x:=e_2]:\tau_2$.
3. 
   - return a >>= f = Just a >>= f = f a
   -  m has two possible values
	   - Nothing >>= return = Nothing
	   - (Just a) >>= return = return a = Just a
   -  Again m has two possible values
	   - (Nothing >>= f) >>= g = Nothing >> g = Nothing = Nothing >>= (\x -> f x >>= g)
	   - (Just a >>= f)>>= g = (f a)>>= g = (\x -> f x >>= g) a = Just a >>= (\x -> f x>>=g)