Add syntax highlighting,

Add table of case studies

bibliography.bib

@@ -438,3 +438,10 @@ @article{leroy-zinc
   author={Leroy, Xavier},
   year={1990}
 }
+
+@article{abel-nbe,
+  title={Normalization by Evaluation: Dependent Types and Impredicativity},
+  author={Abel, Andreas},
+  year={2013}
+}
+

iithesis.cls

@@ -203,8 +203,8 @@
 \newcommand \tw@col [1] {\multicolumn{2}{@{}p{20em}}{#1}}
 
 \RequirePackage[pdftex,unicode=true]{hyperref}
-
-\AtBeginDocument{
+\RequirePackage{etoolbox}
+\AfterEndPreamble{
   \if@pol{\selectlanguage{polish}\old@title{\bfseries\@polishtitle\mdseries}}
          {\selectlanguage{english}\old@title{\bfseries\@englishtitle\mdseries}}
   \let\old@nd\and

main/case-studies.tex

@@ -1,2 +1,37 @@
 \chapter{Case Studies}\label{chapter:case-studies}
-I studied the performance of the algorithm and the implementation on a number of programming language calculi. 
+I studied the performance of the algorithm and the implementation on a number of programming language calculi.
+Figure \ref{fig:tested-interpreters} shows a summary of interpreters on which I tested the transformer.
+The first group of interpreters is denotational (mostly meta-circular) in style and covers various extensions of the base \LC{} with call-by-value evaluation order.
+The additions I tested include: integers with addition, recursive let-bindings, delimited control operators -- \textit{shift} and \textit{reset} with CPS interpreter based on \cite{biernacka-delimited-continuations} and exceptions in two styles: monadic with exceptions as values (functions return either value or an exception) and in CPS with success and error continuations.
+The last interpreter for call-by-value in Figure \ref{fig:tested-interpreters} is a normalization function based on normalization by evaluation technique transcribed from \cite{abel-nbe}.
+The next three interpreters correspond to big-step operational semantics for call-by-name \LC{}, call-by-need (call-by-name with memoization) and a simple imperative language respectively.
+
+\begin{figure}
+\begin{center}
+\begin{tabular}{c|c|c|c}
+Language & Interpreter style & Lang. Features & Result \\
+\Xhline{2\arrayrulewidth}
+\multirow{13}{*}{\makecell{call-by-value \\ \LC{}}} & denotational & $\cdot$ & CEK machine \\
+\cline{2-4}
+& denotational & integers with add & CEK with add \\
+\cline{2-4}
+& \makecell{denotational, \\ recursion via \\ environment} & \makecell{integers, recursive \\ let-bindings} & \makecell{similar to Reynold's  \\ first-order interpreter}\\
+\cline{2-4}
+& \makecell{denotational \\ with conts.} & shift and reset & two layers of conts.\\
+\cline{2-4}
+& \makecell{denotational, \\ monadic} & \multirow{3}{*}{\makecell{exceptions \\ with handlers}} & \makecell{explicit \\ stack unwinding}\\
+\cline{2-2}\cline{4-4}
+& \makecell{denotational, \\ CPS} & & \makecell{pointer to\\ exception handler}\\
+\cline{2-4}
+& \makecell{normalization \\ by evaluation} & $\cdot$ & strong CEK machine \\
+\hline
+\makecell{call-by-name \\ \LC{}} & big-step & $\cdot$ & Krivine machine \\
+\hline
+\makecell{call-by-need \\ \LC{}} & \makecell{big-step \\ (state passing)} & memoization & lazy Krivine machine \\
+\hline
+\makecell{simple \\ imperative} & \makecell{big-step \\ (state passing)} & \makecell{conditionals, \\ while, assignment} & $\cdot$\\
+\hline
+\end{tabular}
+\end{center}
+\caption{Summary of tested interpreters}\label{fig:tested-interpreters}
+\end{figure}

main/functional-correspondence.tex

@@ -41,7 +41,7 @@ \section{Continuation-Passing Style}
 To translate an anonymous function definition, first a fresh variable \texttt{k'} is generated then the body of the function is translated with \texttt{k'} as the continuation and finally, the continuation $k$ is applied to the transformed function expression.
 Function application is transformed by placing all sub-expressions in successively nested functions, with the deepest one actually performing the call with an additional argument -- the continuation $k$.
 This way the evaluation of arguments is sequenced left-to-right and happens before the application.
-Translation of the \texttt{match} expression requires translating the scrutinee and putting the branches in the continuation. The branches are all transformed using the same continuation $k$.
+Translation of the \lstinline{match} expression requires translating the scrutinee and putting the branches in the continuation. The branches are all transformed using the same continuation $k$.
 Finally, during translation of the \texttt{error} expression the continuation is discarded since the error halts the execution.
 The omitted rules for \texttt{if} expressions and record creation are similar to \texttt{match} expressions and applications respectively.
 
@@ -66,21 +66,21 @@ \section{Continuation-Passing Style}
 \begin{figure}
     \centering
    \begin{align*}
-        \llbracket \texttt{x} \rrbracket k =& \texttt{(}k\,\texttt{x)}\\
+        \llbracket \lstinline{x} \rrbracket k =& \lstinline{(}k\,\lstinline{x)}\\
 %
-        \llbracket \texttt{(fun (x y ...) e)} \rrbracket k
-        =& \texttt{(} k \, \texttt{(fun (x y ... k')}\, \llbracket \texttt{e} \rrbracket \texttt{k'))} \\
+        \llbracket \lstinline!(fun ($x \ldots$)$\;e$)! \rrbracket k
+        =& \lstinline{(} k \; \lstinline!(fun ($x \ldots$ k')!\, \llbracket \lstinline{e} \rrbracket \lstinline{k'))} \\
 %        
-        \llbracket \texttt{(}e_1\ldots e_n\texttt{)} \rrbracket k
-        =& \llbracket e_1 \rrbracket \, \texttt{(fun (v1)} \ldots \llbracket e_n \rrbracket k' \ldots \texttt{)}\, \\
-         & \text{where}\,k' = \texttt{(fun (vn) (v1...vn}\,k\texttt{))} \\
+        \llbracket \lstinline{(}e_1\ldots e_n\lstinline{)} \rrbracket k
+        =& \llbracket e_1 \rrbracket \, \lstinline!(fun (v$_1$)! \bb{e_2}\lstinline!(fun$\;$($v_2$)! \ldots \llbracket e_n \rrbracket k' \lstinline!)$\ldots$)!\, \\
+         & \text{where}\,k' = \lstinline!(fun (v$_n$)$\;$(v$_1 \ldots\;$v$_n$!\,k\lstinline!))! \\
 %        
-        \llbracket \texttt{(match } e \texttt{(} p_1\,e_1\texttt{)}\ldots \texttt{(} p_n\,e_n\texttt{)} \rrbracket k
-        =& \llbracket e \rrbracket \texttt{(fun (v) (case v }ps \,\texttt{)}\\
-         & \text{where}\,ps = \texttt{(} p_1\,\llbracket e_1 \rrbracket k  \texttt{)}\ldots \texttt{(} p_n\,\llbracket e_n \rrbracket k \texttt{)}\\
+        \llbracket \lstinline!(match $\;e\;$ ($p\;e'$)$\ldots$)! \rrbracket k
+        =& \llbracket e \rrbracket \lstinline!(fun (v)$\;$(match v\ !ps \lstinline!)!\\
+        & \text{where}\,ps = \lstinline!(!p\;\llbracket e' \rrbracket k \lstinline!)! \ldots \\
 %
-        \llbracket \texttt{(error}\,s\,\texttt{)} \rrbracket k
-        =& \texttt{(error}\,s\,\texttt{)} \\
+%         \llbracket \lstinline{(error}\,s\,\lstinline{)} \rrbracket k
+%         =& \lstinline{(error}\,s\,\lstinline{)}
    \end{align*}
     \caption{A call-by-value CPS translation}
     \label{fig:cps-translation}
@@ -111,14 +111,14 @@ \section{Continuation-Passing Style}
 \end{figure}
 
 \section{Defunctionalization}
-The second step is the elimination of higher order functions from our interpreter, transforming it into a collection of mutually (tail-)recursive functions -- a state machine with the \texttt{main} function building initial configuration.
+The second step is the elimination of higher order functions from our interpreter, transforming it into a collection of mutually (tail-)recursive functions -- a state machine with the \lstinline{main} function building initial configuration.
 There are many approaches to compiling first class functions away but of particular interest to us will be defunctionalization.
 It is a global program transformation that replaces each anonymous function definition with a uniquely labeled record which holds the values for function's free variables.
 Every application of unknown function is replaced with a specific top-level \textit{apply} function which dispatches on the label of the passed record and evaluates the corresponding function's body.
 
 This simple description glosses over many important details.
 Firstly, we must distinguish between known and unknown function calls as only unknown calls should be transformed.
-Secondly, we must be able to create records for top-level definitions when they are passed as a first class function, e.g., in the definition of \texttt{eval} in the branch for variables we apply an unknown function \texttt{env} which may evaluate either to an anonymous function created by \texttt{extend} or a top-level function \texttt{init}.
+Secondly, we must be able to create records for top-level definitions when they are passed as a first class function, e.g., in the definition of \lstinline{eval} in the branch for variables we apply an unknown function \lstinline{env} which may evaluate either to an anonymous function created by \lstinline{extend} or a top-level function \lstinline{init}.
 Lastly, we must somehow know for each application point which functions may be applied.
 The first two challenges can be solved with a static, syntactic analysis of the interpreter.
 The other challenge can be solved using control-flow analysis as described in Section \ref{sec:selective-defun}.

main/introduction.tex

@@ -187,8 +187,8 @@ \subsection*{Big-step Operational Semantics}
 (def init-state (var) 0)
 (def update-state (tgt val state) ...)
 
-(def aval (state aexpr) ...) ; valuate arithmetic expression
-(def bval (state bexpr) ...) ; valuate boolean expression
+(def aval (state aexpr) ...) ;; valuate arithmetic expression
+(def bval (state bexpr) ...) ;; valuate boolean expression
 
 (def eval (state cmd)
   (match cmd

thesis.tex

@@ -1,21 +1,45 @@
 \documentclass[english, mgr, shortabstract]{iithesis}
 
-\usepackage[backend=biber,sorting=nty,language=english]{biblatex}
+\usepackage[backend=biber,sorting=none,language=english]{biblatex}
 \usepackage{amsmath}
 \usepackage{amsfonts}
 \usepackage{stmaryrd}
 \usepackage{listings}
-% \usepackage{fira}
+\usepackage{multirow}
+\usepackage{makecell}
+\usepackage{xcolor}
+
+\usepackage[scale=0.8]{FiraMono}
+
+\lstdefinelanguage{idl}{%
+  alsoletter={-,?,\#,:},
+  otherkeywords={(,),\{,\},[,]},
+  morekeywords={def,fun,def-data,def-struct,match,let,error},
+  morekeywords=[2]{String,Integer,Any,Boolean},
+  morekeywords=[3]{(,),\{,\},[,]},
+  morekeywords=[4]{\#:apply, \#:atomic, \#:no-defun}
+  sensitive=false,
+  morestring=[b]",
+  morecomment=[l]{;;}
+}
 
 \lstset{%
-  basicstyle=\ttfamily,
+  basicstyle=\ttfamily\color{black},
   mathescape=true,
-  escapechar=@
-}
+  showstringspaces=false,
+  keywordstyle={\color{green!50!black}},
+  keywordstyle=[2]{\color{blue!50!black}}, 
+  keywordstyle=[3]{\color{gray}},
+  keywordstyle=[4]{\color{blue!80!black}},
+  commentstyle=\color{gray}\itshape,
+  stringstyle=\color{green!80!black},
+  identifierstyle=\color{black},
+  escapechar=@,
+  language=idl
+} 
 
 % Allows to use lstinline in the math mode
 % See https://tex.stackexchange.com/questions/127010/how-can-i-make-lstinline-function-normally-inside-math-mode
-\usepackage{etoolbox}
 \expandafter\patchcmd\csname \string\lstinline\endcsname{%
   \leavevmode
   \bgroup
@@ -53,11 +77,6 @@
 
 \mathchardef\mh="2D
 
-% define "struts", as suggested by Claudio Beccari in
-%    a piece in TeX and TUG News, Vol. 2, 1993.
-\newcommand\Tstrut{\rule{0pt}{2.6ex}}         % = `top' strut
-\newcommand\Bstrut{\rule[-0.9ex]{0pt}{0pt}}   % = `bottom' strut
-
 \addbibresource{bibliography.bib}
 \DeclareFieldFormat[
   article,inproceedings,incollection,book,misc,report]{title}{#1}