diff --git a/doc/lectures.out b/doc/lectures.out
deleted file mode 100755
index 50ab82cdd..000000000
--- a/doc/lectures.out
+++ /dev/null
@@ -1,25 +0,0 @@
-\BOOKMARK [1][-]{section.1}{Introduction: Languages, Semantics, Interpreters, Compilers}{}% 1
-\BOOKMARK [2][-]{subsection.1.1}{Language and semantics}{section.1}% 2
-\BOOKMARK [2][-]{subsection.1.2}{Interpreters}{section.1}% 3
-\BOOKMARK [2][-]{subsection.1.3}{Compilers}{section.1}% 4
-\BOOKMARK [2][-]{subsection.1.4}{The first example: language of expressions}{section.1}% 5
-\BOOKMARK [1][-]{section.2}{Statements, Stack Machine, Stack Machine Compiler}{}% 6
-\BOOKMARK [2][-]{subsection.2.1}{Statements}{section.2}% 7
-\BOOKMARK [1][-]{section.3}{Stack Machine}{}% 8
-\BOOKMARK [2][-]{subsection.3.1}{A Compiler for the Stack Machine}{section.3}% 9
-\BOOKMARK [1][-]{section.4}{Structural Induction}{}% 10
-\BOOKMARK [2][-]{subsection.4.1}{Structural Control Flow}{section.4}% 11
-\BOOKMARK [2][-]{subsection.4.2}{Extended Stack Machine}{section.4}% 12
-\BOOKMARK [2][-]{subsection.4.3}{Syntax Extensions}{section.4}% 13
-\BOOKMARK [1][-]{section.5}{Procedures}{}% 14
-\BOOKMARK [1][-]{section.6}{Extended Stack Machine}{}% 15
-\BOOKMARK [1][-]{section.7}{Functions}{}% 16
-\BOOKMARK [2][-]{subsection.7.1}{Functions in Expressions}{section.7}% 17
-\BOOKMARK [2][-]{subsection.7.2}{Return Statement}{section.7}% 18
-\BOOKMARK [1][-]{section.8}{Arrays and strings}{}% 19
-\BOOKMARK [2][-]{subsection.8.1}{Adding arrays on expression level}{section.8}% 20
-\BOOKMARK [2][-]{subsection.8.2}{Adding arrays on statement level}{section.8}% 21
-\BOOKMARK [2][-]{subsection.8.3}{Strings}{section.8}% 22
-\BOOKMARK [1][-]{section.9}{S-expressions and Pattern Matching}{}% 23
-\BOOKMARK [2][-]{subsection.9.1}{S-expressions on expression level}{section.9}% 24
-\BOOKMARK [2][-]{subsection.9.2}{Patterns Matching}{section.9}% 25
diff --git a/doc/lectures.pdf b/doc/lectures.pdf
deleted file mode 100755
index 1e2f56b37..000000000
Binary files a/doc/lectures.pdf and /dev/null differ
diff --git a/doc/01.tex b/doc/lectures/01.tex
similarity index 100%
rename from doc/01.tex
rename to doc/lectures/01.tex
diff --git a/doc/02.tex b/doc/lectures/02.tex
similarity index 100%
rename from doc/02.tex
rename to doc/lectures/02.tex
diff --git a/doc/03.tex b/doc/lectures/03.tex
similarity index 100%
rename from doc/03.tex
rename to doc/lectures/03.tex
diff --git a/doc/04.tex b/doc/lectures/04.tex
similarity index 100%
rename from doc/04.tex
rename to doc/lectures/04.tex
diff --git a/doc/05.tex b/doc/lectures/05.tex
similarity index 100%
rename from doc/05.tex
rename to doc/lectures/05.tex
diff --git a/doc/06.tex b/doc/lectures/06.tex
similarity index 100%
rename from doc/06.tex
rename to doc/lectures/06.tex
diff --git a/doc/07.tex b/doc/lectures/07.tex
similarity index 100%
rename from doc/07.tex
rename to doc/lectures/07.tex
diff --git a/doc/08.tex b/doc/lectures/08.tex
similarity index 100%
rename from doc/08.tex
rename to doc/lectures/08.tex
diff --git a/doc/lectures.tex b/doc/lectures/lectures.tex
similarity index 100%
rename from doc/lectures.tex
rename to doc/lectures/lectures.tex
diff --git a/doc/spec/spec.tex b/doc/spec/spec.tex
new file mode 100644
index 000000000..e4f7f8b16
--- /dev/null
+++ b/doc/spec/spec.tex
@@ -0,0 +1,130 @@
+\documentclass{article}
+
+\usepackage{amssymb, amsmath}
+\usepackage{alltt}
+\usepackage{pslatex}
+\usepackage{epigraph}
+\usepackage{verbatim}
+\usepackage{latexsym}
+\usepackage{array}
+\usepackage{comment}
+\usepackage{makeidx}
+\usepackage{listings}
+\usepackage{indentfirst}
+\usepackage{verbatim}
+\usepackage{color}
+\usepackage{url}
+\usepackage{xspace}
+\usepackage{hyperref}
+\usepackage{stmaryrd}
+\usepackage{amsmath, amsthm, amssymb}
+\usepackage{graphicx}
+\usepackage{euscript}
+\usepackage{mathtools}
+\usepackage{mathrsfs}
+\usepackage{multirow,bigdelim}
+\usepackage{subcaption}
+\usepackage{placeins}
+
+\makeatletter
+
+\makeatother
+
+\definecolor{shadecolor}{gray}{1.00}
+\definecolor{darkgray}{gray}{0.30}
+
+\def\transarrow{\xrightarrow}
+\newcommand{\setarrow}[1]{\def\transarrow{#1}}
+
+\def\padding{\phantom{X}}
+\newcommand{\setpadding}[1]{\def\padding{#1}}
+
+\def\subarrow{}
+\newcommand{\setsubarrow}[1]{\def\subarrow{#1}}
+
+\newcommand{\trule}[2]{\frac{#1}{#2}}
+\newcommand{\crule}[3]{\frac{#1}{#2},\;{#3}}
+\newcommand{\withenv}[2]{{#1}\vdash{#2}}
+\newcommand{\trans}[3]{{#1}\transarrow{\padding{\textstyle #2}\padding}\subarrow{#3}}
+\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}\subarrow{#3},\;{#4}}
+\newcommand{\llang}[1]{\mbox{\lstinline[mathescape]|#1|}}
+\newcommand{\pair}[2]{\inbr{{#1}\mid{#2}}}
+\newcommand{\inbr}[1]{\left<{#1}\right>}
+\newcommand{\highlight}[1]{\color{red}{#1}}
+\newcommand{\ruleno}[1]{\eqno[\scriptsize\textsc{#1}]}
+\newcommand{\rulename}[1]{\textsc{#1}}
+\newcommand{\inmath}[1]{\mbox{$#1$}}
+\newcommand{\lfp}[1]{fix_{#1}}
+\newcommand{\gfp}[1]{Fix_{#1}}
+\newcommand{\vsep}{\vspace{-2mm}}
+\newcommand{\supp}[1]{\scriptsize{#1}}
+\newcommand{\sembr}[1]{\llbracket{#1}\rrbracket}
+\newcommand{\cd}[1]{\texttt{#1}}
+\newcommand{\free}[1]{\boxed{#1}}
+\newcommand{\binds}{\;\mapsto\;}
+\newcommand{\dbi}[1]{\mbox{\bf{#1}}}
+\newcommand{\sv}[1]{\mbox{\textbf{#1}}}
+\newcommand{\bnd}[2]{{#1}\mkern-9mu\binds\mkern-9mu{#2}}
+\newtheorem{lemma}{Lemma}
+\newtheorem{theorem}{Theorem}
+\newcommand{\meta}[1]{{\mathcal{#1}}}
+\renewcommand{\emptyset}{\varnothing}
+\newcommand{\dom}[1]{\mathtt{dom}\;{#1}}
+\newcommand{\primi}[2]{\mathbf{#1}\;{#2}}
+
+\definecolor{light-gray}{gray}{0.90}
+\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}}
+
+\lstdefinelanguage{ocaml}{
+keywords={let, begin, end, in, match, type, and, fun, 
+function, try, mod, with, class, object, method, of, rec, repeat, until,
+while, not, do, done, as, val, inherit, module, sig, @type, struct, 
+if, then, else, open, virtual, new, fresh, skip, od, fi, elif, for, local, return, read, write, fi, case, esac, od},
+sensitive=true,
+%basicstyle=\small,
+commentstyle=\scriptsize\rmfamily,
+keywordstyle=\ttfamily\bfseries,
+identifierstyle=\ttfamily,
+basewidth={0.5em,0.5em},
+columns=fixed,
+fontadjust=true,
+literate={->}{{$\to$}}3 {===}{{$\equiv$}}1 {=/=}{{$\not\equiv$}}1 {|>}{{$\triangleright$}}3 {\&\&\&}{{$\wedge$}}2 {|||}{{$\vee$}}2 {^}{{$\uparrow$}}1,
+morecomment=[s]{(*}{*)}
+}
+
+\lstset{
+mathescape=true,
+%basicstyle=\small,
+identifierstyle=\ttfamily,
+keywordstyle=\bfseries,
+commentstyle=\scriptsize\rmfamily,
+basewidth={0.5em,0.5em},
+fontadjust=true,
+escapechar=!,
+language=ocaml
+}
+
+\sloppy
+
+\newcommand{\ocaml}{\texttt{OCaml}\xspace}
+
+\theoremstyle{definition}
+
+\title{Introduction to Programming Languages, Compilers and Tools}
+
+\author{Dmitry Boulytchev}
+
+\begin{document}
+
+\maketitle
+
+\input{01}
+\input{02}
+\input{03}
+\input{04}
+\input{05}
+\input{06}
+\input{07}
+\input{08}
+
+\end{document}