\myheading{Further reading}

There are several interesting open-source attempts to build decompiler.
Both source code and theses are interesting study.

\begin{itemize}
	\item \emph{decomp} by Jim Reuter\footnote{
			\url{http://www.program-transformation.org/Transform/DecompReadMe},
			\url{http://www.program-transformation.org/Transform/DecompDecompiler}}.

	\item \emph{DCC} by Cristina Cifuentes\footnote{
			\url{http://www.program-transformation.org/Transform/DccDecompiler},
			thesis: \url{https://yurichev.com/mirrors/DCC_decompilation_thesis.pdf}}.

		It is interesting that this decompiler supports only one type (\emph{int}).
		Maybe this is a reason why DCC decompiler produces source code with \emph{.B} extension?
		Read more about B typeless language (C predecessor): \url{https://yurichev.com/blog/typeless/}.

	\item \emph{Boomerang} by Mike Van Emmerik, Trent Waddington et al\footnote{
			\url{http://boomerang.sourceforge.net/},
			\url{http://www.program-transformation.org/Transform/MikeVanEmmerik},
			thesis: \url{https://yurichev.com/mirrors/vanEmmerik_ssa.pdf}}.
\end{itemize}

As I've mentioned, LISP knowledge can help to understand this all much easier.
Here is well-known micro-interpreter of LISP by Peter Norvig, also written in Python:
\url{https://web.archive.org/web/20161116133448/http://www.norvig.com/lispy.html},
\url{https://web.archive.org/web/20160305172301/http://norvig.com/lispy2.html}.

The gradual rewriting I've shown here is also available in Mathematica ("Trace" command):
\url{https://reference.wolfram.com/language/ref/Trace.html}.

I also enjoyed reading ``The Elements of Artificial Intelligence'' book by Steve Tanimoto
\footnote{\url{https://archive.org/details/TheElementsOfArtificialIntelligenceUsingLisp/}},
chapter 3: ``Production Systems and Pattern Matching''.

See also: Nuno Lopes -- Verifying Optimizations using SMT Solvers
\footnote{\url{https://llvm.org/devmtg/2013-11/slides/Lopes-SMT.pdf}}.