diff --git a/semester4/fmfp/formal-methods-functional-programming-summary.tex b/semester4/fmfp/formal-methods-functional-programming-summary.tex
index 9e96c57..84b03dd 100644
--- a/semester4/fmfp/formal-methods-functional-programming-summary.tex
+++ b/semester4/fmfp/formal-methods-functional-programming-summary.tex
@@ -68,5 +68,13 @@
 % \input{parts/01_formal-reasoning/05_correctness/}
 % \input{parts/01_formal-reasoning/}
 
+\newsection
+\section{Typing}
+\input{parts/02_typing/00_intro.tex}
+\input{parts/02_typing/01_mini-haskell/00_syntax.tex}
+% \input{parts/02_typing/01_mini-haskell/}
+\input{parts/02_typing/02_lambda-calculus.tex}
+% \input{parts/02_mini-haskell/}
+
 
 \end{document}
diff --git a/semester4/fmfp/parts/02_typing/00_intro.tex b/semester4/fmfp/parts/02_typing/00_intro.tex
new file mode 100644
index 0000000..61c7319
--- /dev/null
+++ b/semester4/fmfp/parts/02_typing/00_intro.tex
@@ -0,0 +1,3 @@
+A great type system is essential for all programming languages, but especially so for functional programming languages.
+
+The issue however is that the problem of deciding which expressions are good and which ones aren't is undecidable.
diff --git a/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex b/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex
new file mode 100644
index 0000000..f520cac
--- /dev/null
+++ b/semester4/fmfp/parts/02_typing/01_mini-haskell/00_syntax.tex
@@ -0,0 +1,4 @@
+\subsection{Mini-Haskell}
+This is a stripped down version of Haskell, used here to explore the type system Haskell uses
+
+\subsubsection{Syntax}
diff --git a/semester4/fmfp/parts/02_typing/02_lambda-calculus.tex b/semester4/fmfp/parts/02_typing/02_lambda-calculus.tex
new file mode 100644
index 0000000..af7c720
--- /dev/null
+++ b/semester4/fmfp/parts/02_typing/02_lambda-calculus.tex
@@ -0,0 +1 @@
+\subsection{Lambda calculus}