diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.pdf b/semester4/fmfp/formal-methods-functional-programming-summary.pdf
index 517d2b3..405b061 100644
Binary files a/semester4/fmfp/formal-methods-functional-programming-summary.pdf and b/semester4/fmfp/formal-methods-functional-programming-summary.pdf differ
diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex
index a82d822..cad04a9 100644
--- a/semester4/fmfp/formal-methods-functional-programming-summary.tex
+++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex
@@ -187,5 +187,7 @@ as well as being mentioned a few times in the rest of the summary.
 % \input{parts/06_exercises/02_fm/}
 % \input{parts/06_exercises/}
 
+\input{parts/06_exercises/03_checklist.tex}
+
 
 \end{document}
diff --git a/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex b/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex
index d91a43b..49c6d71 100644
--- a/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex
+++ b/semester4/fmfp/parts/06_exercises/01_fp/00_eval-strats.tex
@@ -1,10 +1,59 @@
 \subsubsection{Evaluation strategies}
+\begin{examdetails}
+    It is likely that one such task will appear.
+\end{examdetails}
 Evaluation strategies formalize how programming languages evaluate the code.
 Most of the commonly used programming languages use \textit{eager evaluation}, whereas functional programming languages tend to prefer \textit{lazy evaluation}
 
+Tasks typically involve doing the compiler / interpreter's work, evaluating a given statement.
+This can either be full haskell code, or in the mini-Haskell, often with lambda functions instead of pattern matching and recursion,
+as that \textit{tends} to be more challenging due to the possibility of losing track of what you expanded or not.
+An easy way around that is to use different colour highlighters.
+
+
 \paragraph{Lazy Evaluation}
 In Lazy Evaluation, expressions are substituted until all possible values are substituted and the expression is then evaluated.
 
-At the exam, it is likely that one such task will appear.
+\subparagraph{Lambda functions}
+For expressions of form \texttt{t1 t2}, \texttt{t1} is evaluated by substituting every occurrence of the function arguments by \texttt{t2}, without evaluation \texttt{t2},
+e.g. \verb|(\x -> x y) (\x -> x)|, the evaluation will lead to \verb|(\x -> x) y|
+Below a more complicated example, highlighted with colours for you to track what goes where:
+
+\begin{enumerate}
+    \item \texttt{{\color{red} ($\backslash$x ->} {\color{ForestGreen} x ($\backslash$y -> x y)}{\color{red})} {\color{orange} ($\backslash$x -> ($\backslash$y -> y) x)}}
+    \item Substitute \texttt{t2} into \texttt{t1} (no eval):
+          \texttt{{\color{orange} ($\backslash$x -> ($\backslash$y -> y) x)} {\color{ForestGreen}($\backslash$y -> {\color{orange} ($\backslash$x -> ($\backslash$y -> y) x)} y)}}
+    \item Recolour for next changes:
+          \texttt{{\color{orange} ($\backslash$x -> {\color{purple}($\backslash$y -> y)} x)} {\color{ForestGreen}($\backslash$y ->
+                      {\color{Aquamarine} ($\backslash$x -> ($\backslash$y -> y) x)} y)}}
+    \item Substitute again:
+          \texttt{{\color{purple}($\backslash$y -> y)} {\color{ForestGreen}($\backslash$y ->
+                      {\color{Aquamarine} ($\backslash$x -> ($\backslash$y -> y) x)} y)}}
+    \item And again:
+          \texttt{{\color{ForestGreen}($\backslash$y ->
+                      {\color{Aquamarine} ($\backslash$x -> ($\backslash$y -> y) x)} y)}}
+\end{enumerate}
+Now, evaluation stops, because there is nothing left to apply. In some cases, this can go on until you get a final result, but \textit{not always}.
+This evaluation example also makes it evident why using colours can be very handy.
+
+\subparagraph{Pattern Matching}
+Pattern matching is fairly straight forward, however, conditional evaluation requires evaluation to the smallest extent possible to determine the option to pick from.
+
 
 \paragraph{Eager Evaluation}
+For expressions of form \texttt{t1 t2}, \texttt{t1} is evaluated by substituting every occurrence of the function arguments by an \textit{evaluated} \texttt{t2},
+i.e. \texttt{t2} is evaluated \textit{before} substituting it.
+Coming back to the short example from above \verb|(\x -> x y) (\x -> x)| is evaluated to the same \verb|(\x -> x) y|.
+The difference only becomes evident with a more complicated example. We'll use the same example again as above, again highlighted.
+\begin{enumerate}
+    \item \texttt{{\color{red} ($\backslash$x ->} {\color{ForestGreen} x ($\backslash$y -> x y)}{\color{red})} {\color{orange} ($\backslash$x -> ($\backslash$y -> y) x)}}
+    \item Evaluate {\color{orange} orange parts} (now {\color{purple} purple}):
+          \texttt{{\color{red} ($\backslash$x ->} {\color{ForestGreen} x ($\backslash$y -> x y)}{\color{red})} {\color{purple} ($\backslash$x -> x)}}
+    \item Substitute {\color{purple} purple}:
+          \texttt{{\color{ForestGreen} {\color{purple} ($\backslash$x -> x)} ($\backslash$y -> {\color{purple} ($\backslash$x -> x)} y)}}
+    \item Evaluate {\color{ForestGreen} green} parts (now {\color{cyan} cyan}):
+          \texttt{{\color{purple} ($\backslash$x -> x)} {\color{cyan}($\backslash$y -> y)}}
+    \item Substitute {\color{cyan} cyan}:
+          \texttt{{\color{cyan}($\backslash$y -> y)}}
+\end{enumerate}
+As you can clearly see, both strategies don't result in the same evaluation.
diff --git a/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex b/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex
index e69de29..f5dea82 100644
--- a/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex
+++ b/semester4/fmfp/parts/06_exercises/01_fp/01_haskell.tex
@@ -0,0 +1,35 @@
+\subsubsection{Haskell}
+\begin{examdetails}
+    typically either short coding task or proof of program
+\end{examdetails}
+
+\paragraph{Programming}
+The best tip here is to read the Haskell book, and to solve the exercises during the semester.
+
+\subparagraph{Fold}
+One of the most important functions to understand is \texttt{foldr} (and \texttt{foldl}).
+If you have used \texttt{reduce} functions before, in e.g. JavaScript / TypeScript,
+they are similar to a \texttt{map} combined with a \texttt{reduce}.
+
+For instance, in TypeScript, the \texttt{reduce} function has the type signature
+\mint{typescript}|array.reduce( ( accumulator: A, current: A, idx: number, array: A[] ) => A, initialValue: A )|
+
+In the Haskell prelude, they are defined as follows:
+\begin{code}{haskell}
+    foldr :: (a -> b -> b) -> b -> [a] -> b
+    foldr f z []     = z
+    foldr f z (x:xs) = f x (foldr f z xs)
+
+    foldl :: (a -> b -> a) -> a -> [b] -> a
+    foldl f z []     = z
+    foldl f z (x:xs) = foldl f (f v x) xs
+\end{code}
+
+\subparagraph{zipWith}
+To combine a \texttt{map} and a \texttt{zip} function, use \texttt{zipWith}, type:
+\mint{haskell}|zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]|
+
+\TODO Add more remarks
+
+\paragraph{Proofs}
+These proofs use structural induction, see Section~\ref{sec:induction-proofs} for that.
diff --git a/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex b/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex
index e69de29..83a9e23 100644
--- a/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex
+++ b/semester4/fmfp/parts/06_exercises/01_fp/02_natural-deduction.tex
@@ -0,0 +1,52 @@
+\subsubsection{Natural Deduction}
+\paragraph{Parenthesis}
+This task (if it were to even ever appear in the exams) is simply applying precedences, as well as remembering associativity.
+The precedences are as follows:
+\[
+    \neg > \land > \lor > \rightarrow
+\]
+The associativities are right for $\land$ and $\lor$, whereas $\rightarrow$ is left associative. This means that
+\[
+    A \rightarrow B \rightarrow C \text{ is parenthesized as } A \rightarrow (B \rightarrow C)
+\]
+
+
+\paragraph{Derivation trees}
+The most important tip here is to write as little as possible, by defining variables (such as $\Gamma$, $\Gamma'$, etc) for each step,
+so you can simply write that instead of all the content.
+
+
+\paragraph{Defining rules}
+This is often the hardest type of task. First state the obvious cases, the basic introduction and elimination rules according to the given definition.
+Remember that the rules are defined top-down, so, for introducing $A \leftrightarrow B$, defined as $(A \rightarrow B) \land (B \rightarrow A)$, we define the rules as follows:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash (A \rightarrow B) \land (B \rightarrow A)}
+        \infer1[$\leftrightarrow$-intro]{\Gamma \vdash A \leftrightarrow B}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \leftrightarrow B}
+        \infer1[$\leftrightarrow$-elim]{\Gamma \vdash (A \rightarrow B) \land (B \rightarrow A)}
+    \end{prooftree}
+\]
+The hard part is coming up with useful extra rules. Here, and with all rules defined by an AND, we can also define it slightly differently:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \rightarrow B}
+        \hypo{\Gamma \vdash B \rightarrow A}
+        \infer2[$\leftrightarrow$-I]{\Gamma \vdash A \leftrightarrow B}
+    \end{prooftree}
+\]
+Similarly, we can also provide elimination rules for the left or right:
+\[
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \leftrightarrow B}
+        \infer1[$\leftrightarrow$-EL]{\Gamma \vdash (A \rightarrow B)}
+    \end{prooftree}
+    \qquad
+    \begin{prooftree}
+        \hypo{\Gamma \vdash A \leftrightarrow B}
+        \infer1[$\leftrightarrow$-ER]{\Gamma \vdash (B \rightarrow A)}
+    \end{prooftree}
+\]
diff --git a/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex b/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex
index e69de29..d2614fa 100644
--- a/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex
+++ b/semester4/fmfp/parts/06_exercises/01_fp/03_type-inference.tex
@@ -0,0 +1,4 @@
+\subsubsection{Type Inference}
+\begin{enumerate}
+    \item 
+\end{enumerate}
diff --git a/semester4/fmfp/parts/06_exercises/03_checklist.tex b/semester4/fmfp/parts/06_exercises/03_checklist.tex
new file mode 100644
index 0000000..6c9f699
--- /dev/null
+++ b/semester4/fmfp/parts/06_exercises/03_checklist.tex
@@ -0,0 +1,7 @@
+\subsection{Checklist}
+\subsubsection{Learning}
+
+\subsubsection{For the exam}
+\begin{itemize}[label=$\square$]
+    \item Multiple colours of highlighters (for eval tasks)
+\end{itemize}