diff --git a/bin/miniFunPolyInterpreter.ml b/bin/miniFunPolyInterpreter.ml
index 520586c..226b351 100644
--- a/bin/miniFunPolyInterpreter.ml
+++ b/bin/miniFunPolyInterpreter.ml
@@ -75,7 +75,7 @@ let () =
       | Ok ty -> ty
       | Error (`AbsentAssignment msg)
       | Error (`WrongTypeSpecification msg)
-      | Error (`RecusrionsNotImplemented msg)
+      | Error (`RecursionNotImplemented msg)
       | Error (`WrongType msg) ->
         Printf.fprintf stderr "%s\n" msg;
         exit (-1)
diff --git a/lib/miniFun/Lexer.mll b/lib/miniFun/Lexer.mll
index 030df9d..a0a0e25 100644
--- a/lib/miniFun/Lexer.mll
+++ b/lib/miniFun/Lexer.mll
@@ -56,6 +56,7 @@ rule read = parse
   | "+"             {PLUS}
   | ","             {COMMA}
   | "-"             {MINUS}
+  | "?"             {QUESTIONMARK}
   | "->"            {TYPEFUNCTION}
   | "/"             {DIVISION}
   | ":"             {COLUMN}
diff --git a/lib/miniFun/Parser.mly b/lib/miniFun/Parser.mly
index 022d618..e08cb4f 100644
--- a/lib/miniFun/Parser.mly
+++ b/lib/miniFun/Parser.mly
@@ -13,7 +13,7 @@
 %token <int> INT
 %token COMMA COLUMN LEFTPAR RIGHTPAR CMPLESS CMPGREATER PLUS MINUS TIMES
 %token DIVISION MODULO POWER ASSIGNMENT BAND BOR CMP CMPLESSEQ CMPGREATEREQ
-%token FIRST SECOND
+%token FIRST SECOND QUESTIONMARK
 %token EOF
 
 %type <t_exp> prg
@@ -90,6 +90,7 @@ texp:
 typeexp:
   | TYPEINT                               {IntegerType}
   | TYPEBOOL                              {BooleanType}
+  | QUESTIONMARK                          {UnknownType}
   | v = delimited(LEFTPAR, typeexp, RIGHTPAR)
                                           {v}
   | a = typeexp; COMMA; b = typeexp       {TupleType (a, b)}
diff --git a/lib/miniFun/TypeChecker.ml b/lib/miniFun/TypeChecker.ml
index 9fe72f7..8ec63d9 100644
--- a/lib/miniFun/TypeChecker.ml
+++ b/lib/miniFun/TypeChecker.ml
@@ -35,13 +35,13 @@ let rec unify type_a type_b =
       unify a1 b1
 
     | VariableTypeP ({contents = Link ty_link}), ty_rest
-    | ty_rest, VariableTypeP ({contents = Link ty_link})
-      when ty_link = ty_rest ->
-      Ok ()
+    | ty_rest, VariableTypeP ({contents = Link ty_link}) ->
+      unify ty_rest ty_link
 
     | VariableTypeP ({contents = Unbound (a1, _)}),
       VariableTypeP ({contents = Unbound (b1, _)})
       when a1 = b1 ->
+      (* should never happen *)
       Error (`WrongType "Only a single instance of a type should be available.")
 
     | type_ab, VariableTypeP ({contents = Unbound (_id, _level)} as tvar)
@@ -252,7 +252,7 @@ let rec evaluate_type_polimorphic program (env: env) level =
     let generalized_ty = generalize level var_ty in
     evaluate_type_polimorphic rest (VariableMap.add x generalized_ty env) level
   | LetFun (f, xs, _typef, fbody, rest) ->
-    let* _ = Error (`RecusrionsNotImplemented "Let Rec is not implemented.") in
+    let* _ = Error (`RecursionNotImplemented "Let Rec is not implemented.") in
     let tmp_type_f = VariableTypeP (ref (Unbound (new_global_id (), level))) in
     let new_env = VariableMap.add f tmp_type_f env in
     let param_type = VariableTypeP (ref (Unbound (new_global_id (), level))) in
@@ -421,7 +421,7 @@ let typecheck (program: t_exp) : (ftype, [> typechecking_error]) result =
 
 
 let typecheck_polymorphic (program: t_exp)
-  : (type_f, [> typechecking_error]) result =
+  : (type_f, [> polytypechecking_error]) result =
   global_type_id := 0;
   let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in
   let* _ = unifyable type_program (FunctionTypeP (IntegerTypeP, IntegerTypeP))
@@ -430,7 +430,7 @@ let typecheck_polymorphic (program: t_exp)
   Ok (generalized_ty)
 
 let typecheck_polymorphic_unbound (program: t_exp)
-  : (type_f, [> typechecking_error]) result =
+  : (type_f, [> polytypechecking_error]) result =
   global_type_id := 0;
   let* type_program = evaluate_type_polimorphic program VariableMap.empty 0 in
   let generalized_ty = generalize (-1) type_program in
diff --git a/lib/miniFun/TypeChecker.mli b/lib/miniFun/TypeChecker.mli
index e6148e7..63f9d00 100644
--- a/lib/miniFun/TypeChecker.mli
+++ b/lib/miniFun/TypeChecker.mli
@@ -1,5 +1,5 @@
 val typecheck                     : Types.t_exp -> (Types.ftype,  [> Types.typechecking_error]) result
 
-val typecheck_polymorphic         : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result
+val typecheck_polymorphic         : Types.t_exp -> (Types.type_f, [> Types.polytypechecking_error]) result
 
-val typecheck_polymorphic_unbound : Types.t_exp -> (Types.type_f, [> Types.typechecking_error]) result
+val typecheck_polymorphic_unbound : Types.t_exp -> (Types.type_f, [> Types.polytypechecking_error]) result
diff --git a/lib/miniFun/Types.ml b/lib/miniFun/Types.ml
index f8f79da..b2d4869 100644
--- a/lib/miniFun/Types.ml
+++ b/lib/miniFun/Types.ml
@@ -76,6 +76,7 @@ let pp_type_f (ty: type_f) : string =
 type ftype = (* type used for specification *)
     IntegerType
   | BooleanType
+  | UnknownType
   | TupleType of ftype * ftype
   | FunctionType of ftype * ftype
 
@@ -134,9 +135,14 @@ type base_error = [
 type typechecking_error = [
   | base_error
   | `WrongTypeSpecification of string
-  | `RecusrionsNotImplemented of string
 ]
 
+type polytypechecking_error = [
+  | typechecking_error
+  | `RecursionNotImplemented of string
+]
+
+
 type error = [
   | base_error
   | `DivisionByZero of string
diff --git a/lib/miniFun/Types.mli b/lib/miniFun/Types.mli
index 374b6ca..989ddd9 100644
--- a/lib/miniFun/Types.mli
+++ b/lib/miniFun/Types.mli
@@ -34,6 +34,7 @@ val pp_type_f : type_f -> string
 type ftype = (* type used for specification *)
     IntegerType
   | BooleanType
+  | UnknownType
   | TupleType of ftype * ftype
   | FunctionType of ftype * ftype
 
@@ -92,7 +93,11 @@ type base_error = [
 type typechecking_error = [
   | base_error
   | `WrongTypeSpecification of string
-  | `RecusrionsNotImplemented of string
+]
+
+type polytypechecking_error = [
+  | typechecking_error
+  | `RecursionNotImplemented of string
 ]
 
 type error = [
diff --git a/report/document.bib b/report/document.bib
index e69de29..f195369 100644
--- a/report/document.bib
+++ b/report/document.bib
@@ -0,0 +1,19 @@
+@article{MILNER,
+  title = {A theory of type polymorphism in programming},
+  journal = {Journal of Computer and System Sciences},
+  volume = {17},
+  number = {3},
+  pages = {348-375},
+  year = {1978},
+  issn = {0022-0000},
+  doi = {https://doi.org/10.1016/0022-0000(78)90014-4},
+  url = {www.sciencedirect.com/science/article/pii/0022000078900144},
+  author = {Robin Milner},
+}
+
+@inproceedings{REMY,
+  title={Extension of ML type system with a sorted equation theory on types},
+  author={Didier R{\'e}my},
+  year={1992},
+  url={https://api.semanticscholar.org/CorpusID:117549268}
+}
\ No newline at end of file
diff --git a/report/document.pdf b/report/document.pdf
index 7ff15f5..94aa7d2 100644
Binary files a/report/document.pdf and b/report/document.pdf differ
diff --git a/report/document.tex b/report/document.tex
index 4bbd1b5..ba0a418 100644
--- a/report/document.tex
+++ b/report/document.tex
@@ -153,7 +153,7 @@
 \newcommand{\defeq}{\vcentcolon=}
 
 \lstdefinelanguage{miniimp}{
-  keywords={if, then, else, skip, while, do, for, rand},
+  keywords={if, then, else, skip, while, do, for, rand, let},
   keywordstyle=\color{blue}\bfseries,
   identifierstyle=\color{black},
   sensitive=false,
@@ -202,6 +202,8 @@
 
 \input{report}
 
+\printbibliography{}
+
 \end{document}
 
 %% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - %%
diff --git a/report/report.tex b/report/report.tex
index a7f8964..adaa659 100644
--- a/report/report.tex
+++ b/report/report.tex
@@ -426,6 +426,38 @@ output := y;
 
   To see a list of all options run \texttt{dune exec <interpreter> {-}{-} -h}. A binary version of the executables can also be found in the build directory: \href{./_build/default/bin/}{./\_build/default/bin/}.
 \end{section}
+
+
+\begin{section}{Addendum: Algorithm W}
+  Added since the last submission a simplified version of the Algorithm W from {\bf A Theory of Type Polymorphism in Programming}\cite{MILNER}. The implementation uses levels instead of prefexes and does not contain the fixed point as described in {\bf Extension of ML type system with a sorted equation theory on types}\cite{REMY} and \href{https://okmij.org/ftp/ML/generalization.html}{okmij.org/ftp/ML/generalization.html}. Thus \texttt{let rec} is not implemented. But the remaining grammar is fully polimorphically typable.
+  An interpreter that outputs the type of the input program is provided as \href{../bin/miniFunPolyInterpreter.ml}{miniFunPolyInterpreter.ml}. The interpreter admits program that are not functions from integers to integers like with the other interpreter, so the evaluation of the program with input is disabled by default. Otherwise the only possible types of programs would be \(\texttt{Int} \to \texttt{Int}\), \(\forall \texttt{a}, \texttt{a} \to \texttt{Int}\) and \(\forall \texttt{a}, \texttt{a} \to \texttt{a}\) since they can be all unified to \(\texttt{Int} \to \texttt{Int}\).
+  In addition the character \texttt{?} is mapped to the new type \texttt{Unknown}. The new type is not used by the program and any type specification is ignored. The \texttt{?} symbol is just a useful shorthand.
+
+
+  Some examples:
+\begin{lstlisting}
+let f =
+  \z: ? =>
+    \y: ? =>
+      \x: ? =>
+        if x < 0 then y x else z x
+in f
+\end{lstlisting}
+  
+  is correctly evaluated as having the type \( \forall \texttt{a}, (\texttt{Int} \to \texttt{a}) \to (\texttt{Int} \to \texttt{a}) \to \texttt{Int} \to \texttt{a} \).
+
+  \begin{lstlisting}
+let f =
+  \z: ? =>
+    \y: ? =>
+      \x: ? =>
+        if x < 0 then y x else z x
+in
+f (\x: ? => \y: ? => \z: ? => if fst y then snd y else snd z)
+\end{lstlisting}
+  
+is correctly evaluated as having the type \( \forall \texttt{a}\ \texttt{b}, (\texttt{Int} \to (\texttt{Bool}, \texttt{a}) \to (\texttt{b}, \texttt{a}) \to \texttt{a}) \to \texttt{Int} \to (\texttt{Bool}, \texttt{a}) \to (\texttt{b}, \texttt{a}) \to \texttt{a} \).
+\end{section}
 %%% Local Variables:
 %%% TeX-command-extra-options: "-shell-escape"
 %%% TeX-master: "document.tex"