diff --git a/doc/spec/01.introduction.tex b/doc/spec/01.introduction.tex
index 0685f508a..99522309b 100644
--- a/doc/spec/01.introduction.tex
+++ b/doc/spec/01.introduction.tex
@@ -1,10 +1,11 @@
 \chapter{Introduction}
 
-\lama is a programming language developed by JetBrains Research for education purposes. Its general characteristics are:
+\lama is a programming language developed by JetBrains Research for educational purposes as an exemplary language to introduce
+the domain of programming languages, compilers and tools. Its general characteristics are:
 
 \begin{itemize}
 \item procedural with first-class functions~--- functions can be passed as arguments, placed in data structures,
-  returned and constructed at runtime via closures mechanism;
+  returned and ``constructed'' at runtime via closure mechanism;
 \item with lexical static scoping;
 \item strict~--- all arguments of function application are evaluated before function body;
 \item imperative~--- variables can be re-assigned, function calls can have side effects;
@@ -15,9 +16,24 @@
 \end{itemize}
 
 The name \lama is an acronym for $\lambda\textsc{-Algol}$ since the language has borrowed the syntactic shape of
-operators from \textsc{Algol-68}; \textsc{Haskell}~\cite{haskell} and \textsc{OCaml}~\cite{ocaml} can be
+operators from \textsc{Algol-68}~\cite{A68}; \textsc{Haskell}~\cite{haskell} and \textsc{OCaml}~\cite{ocaml} can be
 mentioned as other languages of inspiration.
 
+The main purpose of \lama is to present a repertoire of constructs with certain runtime behavior and
+relevant implementation techniques. The lack of a type system (a vital feature for a real-word language
+for software engineering) is an intensional decision which allows to show the unchained diversity
+of runtime behaviors, including those which a typical type system is called to prevent. On the other hand
+the language can be used in future as a raw substrate to apply various ways of software verification (including
+type systems) on.
+
+The current implementation contains a native code compiler for \textsc{x86-32}, written
+in \textsc{OCaml}, a runtime library with garbage-collection support, written in \textsc{C}, and a small
+standard library, written in \lama itself. The native code compiler uses \textsc{gcc} as a toolchain.
+
+In addition, a source-level reference interpreter is implemented as well as a compiler to a small
+stack machine. The stack machine code can in turn be either interpreted on a stack machine interpreter, or
+used as an intermediate representation by the native code compiler.
+
 %\input{01.01.general_characteristics}
 %\input{01.02.notation}
 %\input{01.03.values}
diff --git a/doc/spec/03.01.lexical_structure.tex b/doc/spec/03.01.lexical_structure.tex
index 550e2fe70..db4e5f322 100644
--- a/doc/spec/03.01.lexical_structure.tex
+++ b/doc/spec/03.01.lexical_structure.tex
@@ -28,7 +28,7 @@ Additionally, two kinds of comments are recognized:
 
 There is a number of specific cases which have to be considered explicitly.
 
-First, block comments can be properly nested. Then, the occurencies of comment symbols inside string literals (see below) are not
+First, block comments can be properly nested. Then, the occurrences of comment symbols inside string literals (see below) are not
 considered as comments.
 
 End-of-line comment encountered \emph{outside} of a block comment escapes block comment symbols:
@@ -91,11 +91,11 @@ Infix operators defined as follows:
 \token{INFIX}=\mbox{\texttt{[+*/\%\$\#@!|\&\^{}~?<>:=\textbackslash-]+}}
 \]
 
-There is a predefined set of built-in infix operators (see~\ref{binary_expressions}); additionally
-an end-used can define custom infix operators (see~\ref{custom_infix}). Note, sometimes 
+There is a predefined set of built-in infix operators (see Fig.~\ref{builtin_infixes}); additionally
+an end-used can define custom infix operators (see Section~\ref{sec:custom_infix}). Note, sometimes 
 additional whitespaces are required to disambiguate infix operator applications. For example, if a
 custom infix operator "\lstinline|+-|" is defined, then the expression "\lstinline|a +- b|" can no longer be
-considered as "\lstinline|a +(-b)|". Note also that a custom operator containing "\lstinline|--|" can not be
+recognized as "\lstinline|a +(-b)|". Note also that a custom operator containing "\lstinline|--|" can not be
 defined due to lexical conventions.
 
 \subsection{Delimiters}
diff --git a/doc/spec/03.02.compilation_units.tex b/doc/spec/03.02.compilation_units.tex
index 0eec2f5cc..eaa0c22e6 100644
--- a/doc/spec/03.02.compilation_units.tex
+++ b/doc/spec/03.02.compilation_units.tex
@@ -1,3 +1,5 @@
+\FloatBarrier
+
 \begin{figure}[t]
   \[
     \begin{array}{rcl}
@@ -12,8 +14,8 @@
 \section{Compilation Units}
 \label{sec:compilation_units}
 
-Compilation unit is a minimal structure recognized by a parser. An application can contain multiple units, compiled separatedly.
-In order to use other units they have to be imported. In particular, the standard library is comprized of a number of precompiled units,
+Compilation unit is a minimal structure recognized by the parser. An application can contain multiple units, compiled separately.
+In order to use other units they have to be imported. In particular, the standard library is comprised of a number of precompiled units,
 which can be imported by an end-user application.
 
 The concrete syntax for compilation unit is shown on Fig.~\ref{compilation_unit}. Besides optional imports a unit must contain
diff --git a/doc/spec/03.03.scope_expressions.tex b/doc/spec/03.03.scope_expressions.tex
index e898d9b12..e98c713e6 100644
--- a/doc/spec/03.03.scope_expressions.tex
+++ b/doc/spec/03.03.scope_expressions.tex
@@ -1,14 +1,17 @@
 \begin{figure}[t]
   \[
-    \begin{array}{rcl}
-      \defterm{scopeExpression}                & : & \nonterm{definition}^\star\s[\s\nonterm{expression}\s]\\
-      \defterm{definition}                     & : & \nonterm{variableDefinition}\alt\nonterm{functionDefinition}\alt\nonterm{infixDefinition}\\
-      \defterm{variableDefinition}             & : & (\s\term{local}\alt\term{public}\s)\s\nonterm{variableDefinitionSequence}\s\term{;}\\
-      \defterm{variableDefinitionSequence}     & : & \nonterm{variableDefinitionSequenceItem}\s(\s\term{,}\s\nonterm{variableDefinitionSequenceItem}\s)^\star\\
-      \defterm{variableDefinitionSequenceItem} & : & \token{LIDENT}\s[\s\term{=}\s\nonterm{basicExpression}\s]\\
-      \defterm{functionDefinition}             & : & [\s\term{public}\s]\s\term{fun}\s\token{LIDENT}\s\term{(}\s\nonterm{functionArguments}\s\term{)}\s\nonterm{functionBody}\\
-      \defterm{functionArguments}              & : & [\s\token{LIDENT}\s(\s\term{,}\s\token{LIDENT}\s)^\star\s]\\
-      \defterm{functionBody}                   & : & \term{\{}\s\nonterm{scopeExpression}\s\term{\}}
+    \begin{array}{rclc}
+      \defterm{scopeExpression}                & : & \nonterm{definition}^\star\s[\s\nonterm{expression}\s]&\\
+      \defterm{definition}                     & : & \nonterm{variableDefinition}&\alt\\
+                                               &   & \nonterm{functionDefinition}&\alt\\
+                                               &   & \nonterm{infixDefinition}&\\
+      \defterm{variableDefinition}             & : & (\s\term{local}\alt\term{public}\s)\s\nonterm{variableDefinitionSequence}\s\term{;}&\\
+      \defterm{variableDefinitionSequence}     & : & \nonterm{variableDefinitionItem}\s(\s\term{,}\s\nonterm{variableDefinitionItem}\s)^\star&\\
+      \defterm{variableDefinitionItem}         & : & \token{LIDENT}\s[\s\term{=}\s\nonterm{basicExpression}\s]&\\
+      \defterm{functionDefinition}             & : & [\s\term{public}\s]\s\term{fun}\s\token{LIDENT}\s\term{(}\s\nonterm{functionArguments}\s\term{)}&\\
+                                               &   & \phantom{XXXXX}\nonterm{functionBody}&\\
+      \defterm{functionArguments}              & : & [\s\token{LIDENT}\s(\s\term{,}\s\token{LIDENT}\s)^\star\s]&\\
+      \defterm{functionBody}                   & : & \term{\{}\s\nonterm{scopeExpression}\s\term{\}}&
     \end{array}
   \]
   \caption{Scope expression concrete syntax}
@@ -75,7 +78,7 @@ However, a definition is a nested scope can override a definition in an enclosin
       skip         -- here x is associated with the function
     };
 
-    skip -- here x is asociated with the variable
+    skip -- here x is associated with the variable
 \end{lstlisting}
 
 A function can freely use all visible definitions; in particular, functions defined in the
@@ -94,10 +97,10 @@ same scope can be mutually recursive:
     skip
 \end{lstlisting}
 
-A variable, defined in a scope, can be attributed with an expression, calcualting its initial value.
+A variable, defined in a scope, can be attributed with an expression, calculating its initial value.
 These expressions, however, are evaluated in the order of variable declaration. Thus, while
 technically it is possible to have forward references in the initialization expression, their
-behaviour is undefined. For example:
+behavior is undefined. For example:
 
 \begin{lstlisting}
     local x = y + 2; -- undefined, as y is not yet initialized at this point
diff --git a/doc/spec/03.04.expressions.tex b/doc/spec/03.04.expressions.tex
index 6b833efdb..cb0e86fdc 100644
--- a/doc/spec/03.04.expressions.tex
+++ b/doc/spec/03.04.expressions.tex
@@ -1,4 +1,81 @@
-\begin{figure}[t]
+\section{Expressions}
+\label{sec:expressions}
+
+The syntax definition for expressions is shown on Fig.~\ref{expressions}. The top-level construct is \emph{sequential composition}, expressed
+using right-associative connective "\term{;}". The basic blocks of sequential composition have the form of \nonterm{binaryExpression}, which is
+a composition of infix operators and operands. The description above is given in a highly ambiguous form as it does not specify explicitly the
+precedence and associativity of infix operators. The precedences and associativity of predefined built-in infix operators are shown
+on Fig.~\ref{builtin_infixes} with the precedence level increasing top-to-bottom.
+
+\begin{figure}[h]
+  \begin{tabular}{c|l|l}
+    infix operator(s) & description & associativity \\
+    \hline
+    \lstinline|:=|                                                                                & assignment                         & right-associative \\
+    \lstinline|:|                                                                                 & list constructor                   & right-associative \\
+    \lstinline|!!|                                                                                & disjunction                        & left-associative  \\
+    \lstinline|&&|                                                                                & conjunction                        & left-associative  \\
+    \lstinline|==|, \lstinline|!=|,  \lstinline|<=|, \lstinline|<|, \lstinline|>=|, \lstinline|>| & integer comparisons                & non-associative   \\
+    \lstinline|+|, \lstinline|-|                                                                  & addition, subtraction              & left-associative  \\
+    \lstinline|*|, \lstinline|/|, \lstinline|%|                                                   & multiplication, quotient, remainder & left-associative
+  \end{tabular}
+\caption{The precedence and associativity of built-in infix operators}
+\label{builtin_infixes}
+\end{figure}
+
+Apart from assignment and list constructor all other built-in infix operators operate on signed integers; in conjunction and disjunction
+any non-zero value is treated as truth and zero as falsity, and the result respects this convention.
+
+The assignment operator is unique among all others in the sense that it requires its left operand to designate a \emph{reference}. This
+property is syntactically ensured using an inference system shown on Fig.~\ref{reference_inference}; here $\mathcal{R}\,(e)$ designates the
+property ``$e$ is a reference''. The result of assignment operator coincides with its right operand, thus
+
+\begin{lstlisting}
+    x := y := 3
+\end{lstlisting}
+
+assigns 3 to both "\lstinline|x|" and "\lstinline|y|".
+
+\begin{figure}[h]
+  \newcommand{\Ref}[1]{\mathcal{R}\,({#1})}
+  \renewcommand{\arraystretch}{4}
+  \[
+    \begin{array}{cc}
+      \Ref{x},\,x\;\mbox{is a variable}&\dfrac{\Ref{e}}{\Ref{\lstinline|$e$ [$\dots$]|}}\\
+      \dfrac{\Ref{e_i}}{\Ref{\mbox{\lstinline|if $\dots$ then $\;e_1\;$ else $\;e_2\;$ fi|}}} & \dfrac{\Ref{e_i}}{\Ref{\mbox{\lstinline|case $\dots$ of $\;\dots\;$ -> $\;e_1\;\dots\;\dots\;$ -> $\;e_k\;$ esac|}}}\\
+      \multicolumn{2}{c}{\dfrac{\Ref{e}}{\Ref{\lstinline|$\dots\;$;$\;e$|}}}
+    \end{array}
+  \]
+  \caption{Reference inference system}
+  \label{reference_inference}
+\end{figure}
+
+\subsection{Postfix Expressions}
+
+There are four postfix forms of expressions:
+
+\begin{itemize}
+\item function call, designated as postfix form "\lstinline|($arg_1, \dots, arg_k$)|";
+\item array element selection, designated as "\lstinline|[$index$]|";
+\item built-in primitive "\lstinline|.string|", returning the string representation of a value;
+\item built-in primitive "\lstinline|.length|", returning the length of a boxed value.
+\end{itemize}
+
+Multiple postfixes are allowed, for example
+
+\begin{lstlisting}
+    x () [3] (1, 2, 3) . string
+    x . string [4]
+    x . length . string
+    x . string . length
+\end{lstlisting}
+
+The basic form of expression is \nonterm{primary}. The simplest form of primary is an identifier or constant. Keywords \lstinline|true| and \lstinline|false|
+designate integer constants 1 and 0 respectively, character constant is implicitly converted into its ASCII code.  String constants designate arrays
+of one-byte characters. Infix constants allow to reference a functional value associated with corresponding infix operator, and functional constant (\emph{lambda-expression})
+designates an anonymous functional value in the form of closure.
+
+\begin{figure}[h]
   \[
     \begin{array}{rcll}
       \defterm{expression}        & : & \nonterm{basicExpression}\s(\s\term{;}\s\nonterm{expression}\s)&\\
@@ -38,91 +115,15 @@
   \label{expressions}
 \end{figure}
 
-\section{Expressions}
-\label{sec:expressions}
-
-\begin{figure}
-  \begin{tabular}{c|l|l}
-    infix operator(s) & description & associativity \\
-    \hline
-    \lstinline|:=|                                                                                & assignment                         & right-associative \\
-    \lstinline|:|                                                                                 & list constructor                   & right-associative \\
-    \lstinline|!!|                                                                                & disjunction                        & left-associative  \\
-    \lstinline|&&|                                                                                & conjunction                        & left-associative  \\
-    \lstinline|==|, \lstinline|!=|,  \lstinline|<=|, \lstinline|<|, \lstinline|>=|, \lstinline|>| & integer comparisons                & non-associative   \\
-    \lstinline|+|, \lstinline|-|                                                                  & addition, subtraction              & left-associative  \\
-    \lstinline|*|, \lstinline|/|, \lstinline|%|                                                   & multiplication, quotent, remainder & left-associative
-  \end{tabular}
-\caption{The precedence and associativity of built-in infix operators}
-\label{builtin_infixes}
-\end{figure}
-
-\begin{figure}
-  \newcommand{\Ref}[1]{\mathcal{R}\,({#1})}
-  \renewcommand{\arraystretch}{4}
-  \[
-    \begin{array}{cc}
-      \Ref{x},\,x\;\mbox{is a variable}&\dfrac{\Ref{e}}{\Ref{\lstinline|$e$ [$\dots$]|}}\\
-      \dfrac{\Ref{e_i}}{\Ref{\mbox{\lstinline|if $\dots$ then $\;e_1\;$ else $\;e_2\;$ fi|}}} & \dfrac{\Ref{e_i}}{\Ref{\mbox{\lstinline|case $\dots$ of $\;\dots\;$ -> $\;e_1\;\dots\;\dots\;$ -> $\;e_k\;$ esac|}}}\\
-      \multicolumn{2}{c}{\dfrac{\Ref{e}}{\Ref{\lstinline|$\dots\;$;$\;e$|}}}
-    \end{array}
-  \]
-  \caption{Reference inference system}
-  \label{reference_inference}
-\end{figure}
-
-The syntax definition for expressions is shown on Fig.~\ref{expressions}. The top-level construct is \emph{sequential composition}, expressed
-using right-associative conective "\term{;}". The basic blocks of sequential composition have the form of \nonterm{binaryExpression}, which is
-a composition of infix operators and operands. The description above is given in a highly ambiguous form as it does not specify explicitly the
-precedence and associativity of infix operators. The precedences and associativity of predefined built-in infix operators are shown
-on Fig.~\ref{builtin_infixes} with the precedence level increasing top-to-bottom.
-
-Apart from assignment and list constructor all other built-in infix operators operate on signed integers; in conjunction and disjunction
-any non-zero value is treated as truth and zero as falsity, and the result respects this convention.
-
-The assignment operator is unique among all others in the sense that it requires its left operand to designate a \emph{reference}. This
-property is syntactically ensured using an inference system shown on Fig.~\ref{reference_inference}; here $\mathcal{R}\,(e)$ designates the
-property ``$e$ is a reference''. The result of assignment operator coincides with its right operand, thus
-
-\begin{lstlisting}
-    x := y := 3
-\end{lstlisting}
-
-assigns 3 to both "\lstinline|x|" and "\lstinline|y|".
-
-\subsection{Postifix Expressions}
-
-There are four postfix forms of expressions:
-
-\begin{itemize}
-\item function call, designated as postfix form "\lstinline|($arg_1, \dots, arg_k$)|";
-\item array element selection, designated as "\lstinline|[$index$]|";
-\item built-in primitive "\lstinline|.string|", returning the string representation of the value;
-\item built-in primitive "\lstinline|.length|", returning the length of boxed value.
-\end{itemize}
-
-Multiple postfixes are allowed, for example
-
-\begin{lstlisting}
-    x () [3] (1, 2, 3) . string
-    x . string [4]
-    x . length . string
-    x . string . length
-\end{lstlisting}
-
-The basic form of expression is \nonterm{primary}. The simplest form of primary is an identifier or constant. Keywords \lstinline|true| and \lstinline|false|
-designate integer constants 1 and 0 respectively, character constant is implicitly converted into its ASCII code.  String constants designate arrays
-of one-byte characters. Infix constants allow to reference a functional value associated with corresponding infix operator, and functional constant (\emph{lambda-expression})
-designates an anonymous functional value in the form of closure.
-
+\FloatBarrier
 \subsection{\texttt{skip} and \texttt{return} Expressions}
 
 Expression \lstinline|skip| can be used to designate a no-value when no action is needed (for example, in the body of unit which contains only declarations).
-\lstinline|return| expression can be used to immediately copmlete the execution of current function call; optional return value can be specified.
+\lstinline|return| expression can be used to immediately complete the execution of current function call; optional return value can be specified.
 
-\subsection{Arrays, Lists, and S-expresions}
+\subsection{Arrays, Lists, and S-expressions}
 
-\begin{figure}[t]
+\begin{figure}[h]
   \[
     \begin{array}{rcl}
       \defterm{arrayExpression} & : & \term{[}\s[\s\nonterm{expression}\s(\s\term{,}\s\nonterm{expression}\s)^\star\s]\s\term{]}\\
@@ -135,12 +136,12 @@ Expression \lstinline|skip| can be used to designate a no-value when no action i
 \end{figure}
 
 There are three forms of expressions to specify composite values: arrays, lists and S-expressions (see Fig.~\ref{composite_expressions}). Note, it is impossible
-to specify one-element list as "\lstinline|{$e$}|" since it is treated as scope expression. Instead, the form "\lstinline|$e$:{}|" can be used; alternatively, standard
-unit "\lstinline|List|" (see~\ref{sec:standard_library_list}) defines function "\lstinline|singleton|" which serves for the same purpose.
+to specify one-element list as "\lstinline|{$e$}|" since it is treated as scope expression. Instead, the form "\lstinline|$e$:{}|" can be used; alternatively, a standard
+unit "\lstinline|List|" (see~Section~\ref{sec:std:list}) defines function "\lstinline|singleton|" which serves for the same purpose.
 
 \subsection{Conditional Expressions}
 
-\begin{figure}[t]
+\begin{figure}[h]
   \[
     \begin{array}{rcll}
       \defterm{ifExpression}  & : & \term{if}\s\nonterm{expression}\s\term{then}\s\nonterm{scopeExpression}\s[\s\nonterm{elsePart}\s]\s\term{fi}&\\
@@ -152,7 +153,7 @@ unit "\lstinline|List|" (see~\ref{sec:standard_library_list}) defines function "
   \label{if_expression}
 \end{figure}
 
-Conditional expression branches the control depending in the value of a certain expression; the value zero is treated as falsity, nonzero as truth. The
+Conditional expression branches the control depending in the value of a certain expression; the value zero is treated as falsity, nonzero as truth. An
 extended form
 
 \begin{lstlisting}
@@ -163,7 +164,7 @@ extended form
     fi
 \end{lstlisting}
 
-is equivalent to the nested form
+is equivalent to a nested form
 
 \begin{lstlisting}
     if $\;c_1\;$ then $\;e1\;$
@@ -173,6 +174,8 @@ is equivalent to the nested form
     fi
 \end{lstlisting}
 
+\FloatBarrier
+
 \subsection{Loop Expressions}
 
 \begin{figure}[t]
@@ -215,7 +218,7 @@ The construct "\lstinline|for $\;i\;$, $\;c\;$, $\;s\;$ do $\;e\;$ od|" is also
 However, the top-level local definitions of the the first expression ("$i$") are visible in the rest of the construct:
 
 \begin{lstlisting}
-    for local i = 0, i < 10, i := i + 1 do write (i) od
+    for local i; i := 0, i < 10, i := i + 1 do write (i) od
 \end{lstlisting}
 
 \subsection{Pattern Matching}
@@ -278,10 +281,10 @@ The semantics of patterns is as follows:
   \item round brackets can be used for grouping.
 \end{itemize}
 
-All identifiers, occured in a pattern, have to be pairwise distinct.
+All identifiers, occurred in a pattern, have to be pairwise distinct.
 
 The matching against patterns in case-expression is performed deterministically in a top-down manner: a pattern
-is matched against only if all previous matchings were unsuccesful. If no matching pattern is found, the execution
+is matched against only if all previous matchings were unsuccessful. If no matching pattern is found, the execution
 of the program stops with an error.
 
 \begin{figure}[t]
@@ -296,16 +299,16 @@ of the program stops with an error.
   \label{case_expression}
 \end{figure}
 
-\subsection{Examples}
-\label{sec:expression_examples}
-
-Some other examples with comments:
-
-\begin{tabular}{ll}
-  "\lstinline|x !! y && z + 3|" & is equivalent to "\lstinline|x !! (y && (z + 3))|"\\
-  "\lstinline|x == y < 4|"      & invalid \\
-  "\lstinline|x [y := 8] := 6|" & is equivalent to "\lstinline|y := 8; x [8] := 6|"\\
-  "\lstinline|(write (3); x) := (write (4); z)|" & is equivalent to "\lstinline|write (3); write (4); x := z|"
-\end{tabular}
+%\subsection{Examples}
+%\label{sec:expression_examples}
+%
+%Some other examples with comments:
+%
+%\begin{tabular}{ll}
+%  "\lstinline|x !! y && z + 3|" & is equivalent to "\lstinline|x !! (y && (z + 3))|"\\
+%  "\lstinline|x == y < 4|"      & invalid \\
+%  "\lstinline|x [y := 8] := 6|" & is equivalent to "\lstinline|y := 8; x [8] := 6|"\\
+%  "\lstinline|(write (3); x) := (write (4); z)|" & is equivalent to "\lstinline|write (3); write (4); x := z|"
+%\end{tabular}
 
 
diff --git a/doc/spec/03.concrete_syntax.tex b/doc/spec/03.concrete_syntax.tex
index 806e54fd7..e64a6ffe2 100644
--- a/doc/spec/03.concrete_syntax.tex
+++ b/doc/spec/03.concrete_syntax.tex
@@ -11,7 +11,7 @@ syntactic description we will use extended Backus-Naur form with the following c
 \item a postfix ``$^\star$'' designates zero-or-more repetitions;
 \item square brackets ``$[\dots]$'' designate zero-or-one repetition;
 \item round brackets ``$(\dots)$'' are used for grouping;
-\item alteration is denoted by ``$\alt$'', sequencing by juxaposition;
+\item alteration is denoted by ``$\alt$'', sequencing by juxtaposition;
 \item a colon ``$:$'' separates a nonterminal being defined from its definition.
 \end{itemize}
 
diff --git a/doc/spec/04.extensions.tex b/doc/spec/04.extensions.tex
index 07976b911..82ac11d8d 100644
--- a/doc/spec/04.extensions.tex
+++ b/doc/spec/04.extensions.tex
@@ -2,8 +2,8 @@
 \label{sec:extensions}
 
 There are some extensions for the core language defined in the previous chapters. These
-extensions add some syntactic sugar, which makes writing programs in \lama a more
-pleasant task.
+extensions add some syntactic sugar, which makes writing programs in \lama a less
+painful task.
 
 \section{Custom Infix Operators}
 \label{sec:custom_infix}
@@ -15,16 +15,16 @@ redefinition of builtin infix operators:
 
 \begin{itemize}
 \item redefinitions of builtin infix operators can not be exported;
-\item assignment operator "\lstinline|:=|" can not be redefined.
+\item the assignment operator "\lstinline|:=|" can not be redefined.
 \end{itemize}
 
 The syntax for infix operator definition is shown on Fig.~\ref{custom_infix_construct}; a custom infix definition must specify exactly two arguments.
 An associativity and precedence level has to be assigned to each custom infix operator. A precedence level is assigned by specifying at which
 position, relative to other known infix operators, the operator being defined is inserted. Three kinds of specifications are allowed: at given level,
-immediately before or immediatly after. For example, "\lstinline|at +|" means that the operator is assigned exactly the same
+immediately before or immediately after. For example, "\lstinline|at +|" means that the operator is assigned exactly the same
 level of precedence as "\lstinline|+|"; "\lstinline|after +|" creates a new precedence level immediately \emph{after} that for
 "\lstinline|+|" (but \emph{before} that for "\lstinline|*|"), and "\lstinline|before *|" has exactly the same effect (provided
-there were no insertions of precedence levels betwee those for "\lstinline|+|" and "\lstinline|*|").
+there were no insertions of precedence levels between those for "\lstinline|+|" and "\lstinline|*|").
 
 When begin inserted at existing precedence level, an infix operator inherits the associativity from that level; hence, only "\lstinline|infix|"
 keyword can be used for such definitions. When a new level is created, an associativity for this level has to be additionally specified
@@ -57,7 +57,7 @@ correspondingly, then importing  "\lstinline|B|" after  "\lstinline|B|" will res
       \defterm{level}           & : & [\s\term{at}\alt\term{before}\alt\term{after}\s]\s\token{INFIX}
     \end{array}
   \]
-  \caption{The Synax for Infix Operator Definition}
+  \caption{The Syntax for Infix Operator Definition}
   \label{custom_infix_construct}
 \end{figure}
 
diff --git a/doc/spec/05.driver_options.tex b/doc/spec/05.driver_options.tex
index 5d0a94ce8..9b20eda58 100644
--- a/doc/spec/05.driver_options.tex
+++ b/doc/spec/05.driver_options.tex
@@ -40,10 +40,10 @@ Additionally, the following options can be given to the driver:
   basename as the source one, with the extension replaced with "\texttt{.ast}".
 \item "\texttt{-ds}"~--- forces the driver to sump stack machine code. The option is only in effect in stack interpreter on
   native mode. The dump is written in the file "\texttt{.sm}".
-\item "\texttt{-v}"~--- makes the dirver to print the version of the compiler.
+\item "\texttt{-v}"~--- makes the driver to print the version of the compiler.
 \item "\texttt{-h}"~--- makes the driver to print the help on the options.
 \end{itemize}
 
 Apart from the paths specified by the "\texttt{-I}" option the driver uses the environment variable "\texttt{LAMA}"
-to locate the runtime and standard libraries (see~\ref{sec:stdlib}). Thus, the units from standard libraries are accessible
+to locate the runtime and standard libraries (see Section~\ref{sec:stdlib}). Thus, the units from standard libraries are accessible
 without any "\texttt{-I}" option given.
diff --git a/doc/spec/06.standard_library.tex b/doc/spec/06.standard_library.tex
index 1d56d54aa..fc3aee912 100644
--- a/doc/spec/06.standard_library.tex
+++ b/doc/spec/06.standard_library.tex
@@ -26,12 +26,12 @@ name of the executable itself).}
 \descr{\lstinline|fun stringcat (list)|}{Takes a list of strings and returns the concatenates all its elements.}
 
 \descr{\lstinline|fun matchSubString (subj, patt, pos)|}{Takes two strings "\lstinline|subj|" and "\lstinline|patt|" and integer position "\lstinline|pos|" and
-checks if a substing of "\lstinline|subj|" starting at position "\lstinline|pos|" is equal to "\lstinline|patt|"; returns integer value.}
+checks if a substring of "\lstinline|subj|" starting at position "\lstinline|pos|" is equal to "\lstinline|patt|"; returns integer value.}
 
 \descr{\lstinline|fun sprintf (fmt, ...)|}{Takes a format string (as per GNU C Library~\cite{GNUCLib}) and a variable number of arguments and
 returns a string, acquired via processing these arguments according to the format string. Note: indexed arguments are not supported.}
 
-\descr{\lstinline|fun substring (str, pos, len)|}{Takes a string, an integer position and length, and returs a substring of requested length of
+\descr{\lstinline|fun substring (str, pos, len)|}{Takes a string, an integer position and length, and returns a substring of requested length of
   given string starting from given position. Raises an error if the original string is shorter then \lstinline|pos+len-1|.}
 
 \descr{\lstinline|infix ++ at + (str1, str2)|}{String concatenation infix operator.}
@@ -130,8 +130,7 @@ returned.}
 no binding is found, and "\lstinline|Some (v)|" if "\lstinline|k|" is bound to "\lstinline|v|".}
 
 \descr{\lstinline|fun removeMap (m, k)|}{Removes the binding for "\lstinline|k|" from the map "\lstinline|m|" and returns a new map. This function
-restores a value which was previously bound to "\lstinline|k|". If there were no binding for "\lstinline|k|" in "\lstinline|m|" then "\lstinline|m|"
-is returned unchanged.}
+restores a value which was previously bound to "\lstinline|k|".}
 
 \descr{\lstinline|fun bindings (m)|}{Returns all bindings for the map "\lstinline|m|" as a list of key-value pairs, in key-ascending order.}
 
@@ -156,8 +155,7 @@ Sets are immutable structures with the following interface:
 \descr{\lstinline|fun memSet (s, v)|}{Tests if an element "\lstinline|v|" is contained in the set "\lstinline|s|". Returns zero if
 there is no such element and non-zero otherwise.}
 
-\descr{\lstinline|fun removeSet (s, v)|}{Removes an element "\lstinline|v|" from the set "\lstinline|s|" and returns a new set. Returns the
-same set if there were nothing to remove.}
+\descr{\lstinline|fun removeSet (s, v)|}{Removes an element "\lstinline|v|" from the set "\lstinline|s|" and returns a new set.}
 
 \descr{\lstinline|fun elements (s)|}{Returns a list of elements of a given set in ascending order.}
 
@@ -174,7 +172,7 @@ enumerated in ascending order.}
 \descr{\lstinline|fun mapSet (f, s)|}{Applies a function "\lstinline|f|" to each element of the set "\lstinline|s|" and returns a new set of images. The
 elements are enumerated in an ascending order.}
 
-\descr{\lstinline|fun foldSet (f, acc, s)|}{Folds a set "\lstinline|s|" unsing the function "\lstinline|f|" and initial value "\lstinline|acc|". The function
+\descr{\lstinline|fun foldSet (f, acc, s)|}{Folds a set "\lstinline|s|" using the function "\lstinline|f|" and initial value "\lstinline|acc|". The function
 "\lstinline|f|" takes two arguments~--- an accumulator and an element of the set. The elements of set are enumerated in an ascending order.}
 
 \subsection{Memoization Tables}
@@ -202,7 +200,7 @@ new hash table.}
 if no binding is found and "\lstinline|Some (v)|" otherwise, where "\lstinline|v|" is a bound value.}
 
 \descr{\lstinline|fun removeHashTab (t, k)|}{Removes a binding for the key "\lstinline|k|" from hash table "\lstinline|t|" and returns a new hash table.
-  The previous binding for "\lstinline|k|" (if any) is restored. If there is no binding for "\lstinline|k|" returns unchanged hash table.}
+  The previous binding for "\lstinline|k|" (if any) is restored.}
 
 \section{Unit \texttt{Fun}}
 
@@ -233,7 +231,7 @@ The unit defines some generic functional stuff:
 }
 
 \section{Unit \texttt{Lazy}}
-\label{sec:lazy}
+\label{sec:std:lazy}
 
 The unit provides primitives for lazy evaluation.
 
@@ -242,6 +240,7 @@ The unit provides primitives for lazy evaluation.
 \descr{\lstinline|fun force (f)|}{Returns a suspended value, forcing its evaluation if needed.}
 
 \section{Unit \texttt{List}}
+\label{sec:std:list}
 
 The unit provides some list-manipulation functions. None of the functions mutate their arguments.
 
diff --git a/doc/spec/Makefile b/doc/spec/Makefile
index 830c3ea7f..52d3b6274 100644
--- a/doc/spec/Makefile
+++ b/doc/spec/Makefile
@@ -1,7 +1,7 @@
 all: metagen
-	pdflatex spec.tex
-	bibtex spec
-	pdflatex spec.tex
+	pdflatex lama-spec.tex
+	bibtex lama-spec
+	pdflatex lama-spec.tex
 
 metagen:
 	git rev-parse --verify HEAD | LC_TIME=en_US.UTF-8 git show --no-patch --no-notes --pretty='%cd' --date=format:"%B, %e, %Y" > commitdate.tex
diff --git a/doc/spec/spec.bib b/doc/spec/lama-spec.bib
similarity index 77%
rename from doc/spec/spec.bib
rename to doc/spec/lama-spec.bib
index e29a91ce7..826af96bd 100644
--- a/doc/spec/spec.bib
+++ b/doc/spec/lama-spec.bib
@@ -1,15 +1,35 @@
+@book{A68,
+author = {Wijngaarden, A. van},
+title = {Report on the Algorithmic Language ALGOL 68},
+year = {1969},
+isbn = {B0007IUUXM},
+publisher = {Printing by the Mathematisch Centrum}
+}
+
+@manual{OCaml,
+  title =        "{OCaml Language}",
+  bibdate =      "February 17, 2020",
+  url     =    "https://www.ocaml.org"
+}
+
+@manual{Haskell,
+  title =        "{Haskell Language}",
+  bibdate =      "February 17, 2020",
+  url =    "https://www.haskell.org"
+}
+
 @manual{GNULib,
   title =        "{The GNU Portability Library}",
   organization = "{Free Software Foundation}",
   bibdate =      "February 24, 2019",
-  bibsource =    "https://www.gnu.org/software/gnulib/manual"
+  url =    "https://www.gnu.org/software/gnulib/manual"
 }
 
 @manual{GNUCLib,
   title =        "{The GNU C Library}",
   organization = "{Free Software Foundation}",
   bibdate =      "February 1, 2020",
-  bibsource =    "https://www.gnu.org/software/libc/manual"
+  url =    "https://www.gnu.org/software/libc/manual"
 }
 
 @inproceedings{HashConsing,
diff --git a/doc/spec/spec.tex b/doc/spec/lama-spec.tex
similarity index 99%
rename from doc/spec/spec.tex
rename to doc/spec/lama-spec.tex
index 7de807ccb..6f61dd79c 100644
--- a/doc/spec/spec.tex
+++ b/doc/spec/lama-spec.tex
@@ -202,6 +202,6 @@ language=alm
 \input{06.standard_library}
 
 \bibliographystyle{plainurl}
-\bibliography{spec}
+\bibliography{lama-spec}
 
 \end{document}