Cleanup of Niki's MPLA thesis

.gitignore

+*~
+\#*\#
+*.bak
+*.backup
+.*.sw[a-z]
+
+.DS_Store
+Thumbs.db*
+
+*.aux
+*.fls
+*.log
+*.out
+*.fdb_latexmk
+*.bbl
+*.blg
+*.toc
+*.tof
+
+thesis.pdf

Makefile

-.PHONY: FORCE default clean distclean
+.PHONY: FORCE lenny all clean distclean
 
-FILE=test
+TARGET=thesis
+.SUFFIXES: .pdf .ps .dvi .tex
 
-export SHELL=/bin/bash
-export TEXINPUTS:=.:./Styles//:${TEXINPUTS}
-export BSTINPUTS:=.:./Styles//:${BSTINPUTS}
+STY = ndisplay.sty liquidHaskell.sty ngrammar.sty
+TEX = theorems.tex grammar.tex typing.tex operational.tex definitions.tex prfLmTransD.tex prfLmTransP.tex proofType.tex
+BIB = myrefs
+SRCFILES = Makefile ${TEX} ${STY} ${BIB}.bib  
 
-default: $(FILE).pdf
+export TEXINPUTS:=${PWD}/Styles//:${TEXINPUTS}
+export BSTINPUTS:=${PWD}/Styles//:${BSTINPUTS}
+export SHELL := /bin/bash
 
-%.pdf: %.tex FORCE
+# make pdf by default
+all: ${TARGET}.pdf
+
+${TARGET}.pdf: ${TARGET}.tex FORCE
 	latexmk -pdf -f -e '$$pdflatex=q/xelatex %O %S/' $<
 
+count:
+	pdftotext $(TARGET).pdf -| tr -d '.' | wc -w
+
 clean:
-	$(RM) *.{dvi,aux,log,toc,lof,lol,lot,dlog,bbl,blg,idx,out,tpt,svn}
-	$(RM) *.{nav,snm,vrb,fls,fdb_latexmk} *~ *.bak
+	$(RM) *.log *.aux *.ps *.dvi *.bbl *.blg *.bak *.fdb_latexmk *~
+
+reallyclean: clean
+	$(RM) $(TARGET).ps $(TARGET).pdf
+
+distclean: reallyclean
 
-distclean: clean
-	$(RM) $(FILE).{dvi,ps,pdf}
+pdfshow: $(TARGET).pdf
+	xpdf $(TARGET).pdf
 
+acroshow: $(TARGET).pdf
+	acroread $(TARGET).pdf
 
+pack: reallyclean
+	tar cvfz liquidHaskell_tex.tar.gz ${SRCFILES}
 
+PHONY : ps all clean reallyclean distclean

Makefile.good

-TEXINPUTS=.:Styles//::
-BSTINPUTS=.:Styles//::
-
-TARGET=main
-STY = ndisplay.sty liquidHaskell.sty ngrammar.sty
-TEX = theorems.tex grammar.tex typing.tex operational.tex definitions.tex prfLmTransD.tex prfLmTransP.tex proofType.tex
-BIB = myrefs
-SRCFILES = Makefile  ${TEX} ${STY} ${BIB}.bib  
-
-
-
-
-# make pdf by default
-# all: ${TARGET}.pdf
-
-all:
-	pdflatex main
-	bibtex main
-	pdflatex main
-	bibtex main
-	pdflatex main
-
-count:
-	pdftotext main.pdf -| tr -d '.' | wc -w
-
-clean:
-	$(RM) *.log *.aux *.ps *.dvi *.bbl *.blg *.bak *.fdb_latexmk *~
-
-reallyclean: clean
-	$(RM) *.ps *.pdf
-
-distclean: reallyclean
-
-pdfshow: $(TARGET).pdf
-	xpdf $(TARGET).pdf
-
-acroshow: $(TARGET).pdf
-	acroread $(TARGET).pdf
-
-pack: reallyclean
-	tar cvfz liquidHaskell_tex.tar.gz ${SRCFILES}
-
-PHONY : ps all clean reallyclean distclean

Makefile.old

-FILES=bytestring.tex \
-	  discussion.tex \
-	  haskellListings.tex \
-	  intro.tex \
-	  xmonad.tex \
-	  related.tex \
-	  termination.tex \
-	  totality.tex \
-	  conclusion.tex \
-	  evaluation.tex \
-	  hscolour.tex \
-	  main.tex \
-	  memory-safety.tex \
-	  results.tex \
-	  text.tex \
-	  type-classes.tex
-
-all: $(FILES)
-	pdflatex main
-	pdflatex main
-	bibtex main
-	pdflatex main
-	bibtex main
-	pdflatex main
-
-clean:
-	$(RM) *.log *.aux *.ps *.dvi *.bbl *.blg *.bak *.fdb_latexmk *.out *~ proofs/*.log
-

abstract_refinements.tex

@@ -351,7 +351,7 @@ or efficiently compute a Fibonacci number.
 %
 
 
-\section{Recursive Invariants}\label{sec:abstract}
+\section{Recursive Invariants}
 Finally, we describe how we use abstract refinements to reason about 
 properties of recursive data structures.
 %
@@ -422,8 +422,8 @@ type IncrList a = List <{\h v -> h <= v}> a
 We can describe different list properties,
 by embedding appropriate concrete refinements.
 For instance, if we use a refinement that expresses that each value 
-is less than the head, i.e., \hbox{@{\h v -> h >= v}@} or 
-different from it, i.e., \hbox{@{\h v -> h ~= v}@},
+is less than the head, i.e., @{\h v -> h >= v}@ or 
+different from it, i.e., @{\h v -> h ~= v}@,
 we can describe decreasing or unique element lists.
 
 \mypara{Using Lists}
@@ -515,7 +515,7 @@ $$
 \end{array}
 $$
 \caption{\textbf{Syntax of Expressions, Types and Schemas}}
-\label{fig:syntax}
+\label{fig:syntax1}
 \end{figure}
 
 
@@ -550,5 +550,5 @@ $$
    [\tsubBase]
 $$
 \caption{\textbf{Static Semantics} from $\lambda_C$ to $\lambda_A$}
-\label{fig:rules}
+\label{fig:rules1}
 \end{figure}

conclusion.tex

 \chapter{Conclusion}
-In this report we presented various refinement type systems.
+In this thesis we presented various refinement type systems.
 We started with type systems where the refinement language expresses arbitrary program expressions.
 Even though these systems are expressive, the assertions formed can not be statically
 verified. 

dependent.tex

@@ -212,7 +212,7 @@ Finally, we define a typing environment $\Gamma$ that maps variables to their ty
 and will be used in the typing rules that we will discuss.
 
 
-\begin{figure}[t!]
+\begin{figure}
 \centering
 $$
 \begin{array}{rrcl}
@@ -358,7 +358,7 @@ In the rest of this paper, we will use the core calculus $\lambda_C$
 upon which we will build a subset of three typing systems~\cite{LiquidPLDI08, Greenberg12, Vazou13}.
 
 
-\begin{figure}[ht!]
+\begin{figure}
 \medskip \judgementHead{Type Checking}{$\hastype{\Gamma}{e}{\tau}$}
 \begin{comment}
 $$\begin{array}{cc}

evaluation.tex

 \section{Evaluation}\label{sec:evaluation}
 
-% We implemented our technique by extending \toolname~\cite{vazou13}. 
+% We implemented our technique by extending \toolname~\cite{Vazou13}. 
 % Next, we describe the tool, the benchmarks, 
 % and a quantitative summary of our results.
 % We then present a qualitative discussion 
@@ -36,7 +36,7 @@
 %       functions terminate and return well ordered trees,
 % \item \texttt{Data.Map.Base}, which implements a functional 
 %       map data type; we verify that all interface functions 
-%       terminate and return binary-search ordered trees~\cite{vazou13}, 
+%       terminate and return binary-search ordered trees~\cite{Vazou13}, 
 % \item \libvectoralgos, which includes a suite of 
 %       ``imperative'' (\ie monadic) array-based sorting algorithms; 
 %       we verify the correctness of vector accessing, indexing, and slicing.
@@ -78,7 +78,7 @@ We have used the following libraries as benchmarks:
       functions terminate and return well ordered trees,
 \item \texttt{Data.Map.Base}, which implements a functional 
       map data type; we verify that all interface functions 
-      terminate and return binary-search ordered trees~\cite{vazou13}, 
+      terminate and return binary-search ordered trees~\cite{Vazou13}, 
 \item \texttt{HsColour}, a syntax highlighting program for Haskell code, we
       verify totality of all functions (\S~\ref{sec:totality}),
 \item \texttt{XMonad}, a tiling window manager for X11, we verify the uniqueness

liquid.tex

@@ -100,7 +100,7 @@ generation and SMT solvers for constraint solving.
 \textit{Satisfiability Modulo Theories} (SMT) solvers solve implications 
 for (fragments of) first-order logic plus various standard theories such as
 equality, real and integer (linear) arithmetic, uninterpreted functions, bit vectors, and (extensional) arrays. 
-Some of the leading systems include  CVC3~\cite{CVC3}, Yices~\cite{Yices}, and Z3~\cite{z3}.
+Some of the leading systems include  CVC3~\cite{CVC3}, Yices~\cite{Yices}, and Z3~\cite{Z3}.
 
 % EXTENSIONS
 With the advent of SMT solvers, 
@@ -141,7 +141,7 @@ to prove specification checking.
 %\item \cite{} 
 %\end{itemize}
 %
-%AND SITE Z3 \cite{z3}
+%AND SITE Z3 \cite{Z3}
 %}
 
 \section{Liquid Types}\label{subsec:liquid}
@@ -362,7 +362,7 @@ the subtyping relation is decidable
 because the refinement language, 
 and thus the implications created, refer to a decidable logic.
 Finally, the \texttt{Valid} relation is evaluated using 
-the Z3~\cite{z3} SMT solver.
+the Z3~\cite{Z3} SMT solver.
 \begin{figure}[ht!]
 \centering
 $$
@@ -389,5 +389,5 @@ $$\begin{array}{cc}
   [\tsub]
 \end{array}$$
 \caption{\textbf{Static Semantics} from $\lambda_C$ to $\lambda_L$}
-\label{fig:rules}
+\label{fig:rules2}
 \end{figure}
\ No newline at end of file

related.tex

@@ -37,7 +37,7 @@ to allow type inference, a crucial feature of a usable type system.
 %
 Even though the language of refinements is restricted,
 as we presented, the combination of
-Abstract Refinements~\cite{vazou13} 
+Abstract Refinements~\cite{Vazou13} 
 with sophisticated measure definitions 
 allows specification and verification of a wide variety 
 of program properties.

structures.tex

@@ -8,7 +8,7 @@ and statically verify critical application specific correctness properties,
 using two illustrative case studies: red-black trees, and the stack-set data
 structure introduced in the \lbxmonad system.
 
-\subsection{Red-Black Trees}\label{sec:redblack}
+\section{Red-Black Trees}\label{sec:redblack}
 
 Red-Black trees have several non-trivial invariants that are ideal for 
 illustrating the effectiveness of refinement types, and contrasting with
@@ -140,7 +140,7 @@ Given the above -- and suitable signatures \toolname
 verifies the various insertion, deletion and rebalancing
 procedures for a Red-Black Tree library.
 
-\subsection{Stack Sets in XMonad}\label{sec:xmonad}
+\section{Stack Sets in XMonad}\label{sec:xmonad}
 
 \lbxmonad is a dynamically tiling \texttt{X11} 
 window manager that is written and configured in Haskell. 

termination.tex

@@ -272,7 +272,7 @@ When @qpart@ finishes partitioning it mutually recursively
 calls @qsort@ to sort the two list and appends the results 
 with @app@. 
 %
-\toolname proves sortedness as well~\cite{vazou13} but let us 
+\toolname proves sortedness as well~\cite{Vazou13} but let us 
 focus here on termination. To this end, we type the functions
 as:
 %
@@ -288,7 +288,7 @@ As before, \toolname checks that at each recursive call
 the caller's metric is less than the callee's. 
 %
 When @qsort@ calls @qpart@ the length of the unsorted 
-list @len (x:xs)@ exceeds the \hbox{@len xs + len [] + len []@}.
+list @len (x:xs)@ exceeds @len xs + len [] + len []@.
 %
 When @qpart@ recursively calls itself the first component
 of the metric is the same, but the length of the unpartitioned 
@@ -299,7 +299,7 @@ exceeds both @len l@ and @len r@, thereby ensuring termination.
 
 
 %%% Before we dive into proving termination, note that the 
-%%% type alias @OL a@ uses Abstract Refinements~\citep{vazou13} to describe 
+%%% type alias @OL a@ uses Abstract Refinements~\citep{Vazou13} to describe 
 %%% Ordered Lists. 
 %%% Thus, when \toolname decides that the @qsort@ is SAFE, 
 %%% it proves both termination and sortedness.

test.bbl

-\providecommand\nbibitem[5][]{\bibitem[#1]{#2}}
-\begin{thebibliography}{Swam11}
-
-\nbibitem[Augu98]{cayenne}{}{}{}
-L.~Augustsson,
-\newblock ``Cayenne - a Language with Dependent Types.'',
-\newblock in {\em ICFP}, 1998.
-
-\nbibitem[Barr07]{CVC3}{}{}{}
-Clark Barrett and Cesare Tinelli,
-\newblock ``{CVC3}'',
-\newblock in Werner Damm and Holger Hermanns, editors, {\em Proceedings of the
-  $19^{th}$ International Conference on Computer Aided Verification (CAV '07)},
-  vol.\ 4590 of {\em Lecture Notes in Computer Science}, pp.\ 298--302,
-  Springer-Verlag, July 2007.
-\newblock Berlin, Germany.
-
-\nbibitem[Barr10]{SMTLIB2}{}{}{}
-C.~Barrett, A.~Stump and C.~Tinelli,
-\newblock ``The {SMT-LIB} {S}tandard: {V}ersion 2.0'',
-\newblock 2010.
-
-\nbibitem[Barr11]{CVC4}{}{}{}
-C.~Barrett, C.~Conway, M.~Deters, L.~Hadarean, D.~Jovanovi\'{c}, T.~King,
-  A.~Reynolds and C.~Tinelli,
-\newblock ``{CVC4}'',
-\newblock in {\em CAV}, 2011.
-
-\nbibitem[Belo11]{Greenberg11}{}{}{}
-J.~F. Belo, M.~Greenberg, A.~Igarashi and B.~C. Pierce,
-\newblock ``Polymorphic Contracts'',
-\newblock in {\em ESOP}, 2011.
-
-\nbibitem[Bert04]{coq-book}{}{}{}
-Y.~Bertot and P.~Cast\'eran,
-\newblock {\em Coq'Art: The Calculus of Inductive Constructions},
-\newblock Springer Verlag, 2004.
-
-\nbibitem[Bier10]{dminor}{}{}{}
-Gavin~M. Bierman, Andrew~D. Gordon, Catalin Hritcu and David~E. Langworthy,
-\newblock ``Semantic subtyping with an SMT solver'',
-\newblock in {\em ICFP}, 2010.
-
-\nbibitem[Blum06]{BlumeM06}{}{}{}
-Matthias Blume and David~A. McAllester,
-\newblock ``Sound and complete models of contracts'',
-\newblock {\em J. Funct. Program.}, vol.~16, no.\ 4-5, pp.\ 375--414, 2006.
-
-\nbibitem[Bozz05]{MathSat}{}{}{}
-M.~Bozzano, R.~Bruttomesso, A.~Cimatti, T.~Junttila, P.~Rossum, S.~Schulz and
-  R.~Sebastiani,
-\newblock ``{MathSAT}: Tight Integration of {SAT} and Mathematical Decision
-  Procedures'',
-\newblock {\em J. Autom. Reason.}, 2005.
-
-\nbibitem[Chit07]{ChitilH07}{}{}{}
-Olaf Chitil and Frank Huch,
-\newblock ``Monadic, Prompt Lazy Assertions in Haskell'',
-\newblock in {\em APLAS}, pp.\ 38--53, 2007.
-
-\nbibitem[Cons86]{Constable86}{}{}{}
-R.L. Constable,
-\newblock {\em Implementing Mathematics with the Nuprl Proof Development
-  System},
-\newblock Prentice-Hall, 1986.
-
-\nbibitem[cpdt13]{cpdt}{}{}{}
-{\em Certified Programming with Dependent Types},
-\newblock MIT Press, 2013.
-
-\nbibitem[dMou08]{z3}{}{}{}
-L.~de~Moura and N.~Bj{\o}rner,
-\newblock ``Z3: An Efficient {SMT} Solver'',
-\newblock 2008.
-
-\nbibitem[Dute]{Yices}{}{}{}
-B.~Dutertre and L.~De Moura,
-\newblock ``Yices {SMT} Solver''.
-\newblock \url{http://yices.csl.sri.com/}.
-
-\nbibitem[Find02]{Findler02}{}{}{}
-R.~B. Findler and M.~Felleisen,
-\newblock ``Contracts for higher-order functions.'',
-\newblock in {\em ICFP}, pp.\ 48--59, 2002.
-
-\nbibitem[Flan06]{flanagan06}{}{}{}
-C.~Flanagan,
-\newblock ``Hybrid Type Checking'',
-\newblock in {\em POPL}, 2006.
-
-\nbibitem[Free91]{FreemanPfenning91}{}{}{}
-T.~Freeman and F.~Pfenning,
-\newblock ``Refinement Types for {ML}'',
-\newblock in {\em PLDI}, 1991.
-
-\nbibitem[Gree12]{Greenberg12}{}{}{}
-M.~Greenberg, B.~C. Pierce and S.~Weirich,
-\newblock ``Contracts Made Manifest'',
-\newblock {\em JFP}, 2012.
-
-\nbibitem[Gron06]{Gronski06}{}{}{}
-Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen~N. Freund and Cormac
-  Flanagan,
-\newblock ``Sage: Hybrid checking for flexible specifications'',
-\newblock in {\em Scheme and Functional Programming Workshop}, pp.\ 93--104,
-  2006.
-
-\nbibitem[Guha07]{GuhaMFK07}{}{}{}
-Arjun Guha, Jacob Matthews, Robert~Bruce Findler and Shriram Krishnamurthi,
-\newblock ``Relationally-parametric polymorphic contracts'',
-\newblock in {\em DLS}, pp.\ 29--40, 2007.
-
-\nbibitem[Hinz06]{Hinze06}{}{}{}
-Ralf Hinze, Johan Jeuring and Andres L{\"o}h,
-\newblock ``Typed Contracts for Functional Programming'',
-\newblock in {\em FLOPS}, pp.\ 208--225, 2006.
-
-\nbibitem[Huet97]{zipper}{}{}{}
-G.~P. Huet,
-\newblock ``The {Z}ipper'',
-\newblock {\em J. Funct. Program.}, 1997.
-
-\nbibitem[Kahr01]{Kahrs01}{}{}{}
-S.~Kahrs,
-\newblock ``Red-black trees with types'',
-\newblock {\em J. Funct. Program.}, 2001.
-
-\nbibitem[Kawa09]{LiquidPLDI09}{}{}{}
-M.~Kawaguchi, P.~Rondon and R.~Jhala,
-\newblock ``Type-based Data Structure Verification'',
-\newblock in {\em PLDI}, 2009.
-
-\nbibitem[Kawa12]{Kawaguchi12}{}{}{}
-Ming Kawaguchi, Patrick~Maxim Rondon, Alexander Bakst and Ranjit Jhala,
-\newblock ``Deterministic parallelism via liquid effects'',
-\newblock in {\em PLDI}, pp.\ 45--54, 2012.
-
-\nbibitem[Lams00]{Lamsweerde00}{}{}{}
-Axel~Van Lamsweerde,
-\newblock ``Formal Specification: a Roadmap'', 2000.
-
-\nbibitem[Mand03]{MandelbaumWalker03}{}{}{}
-Yitzhak Mandelbaum, David Walker and Robert Harper,
-\newblock ``An effective theory of type refinements.'',
-\newblock in {\em ICFP}, pp.\ 213--225, 2003.
-
-\nbibitem[Meye91]{Eiffel}{}{}{}
-B.~Meyer,
-\newblock {\em Eiffel: The Language},
-\newblock Prentice-Hall, 1991.
-
-\nbibitem[Meye92]{Meyer92}{}{}{}
-B.~Meyer,
-\newblock ``Applying "Design by Contract".'',
-\newblock {\em IEEE Computer}, vol.~25, no.~10, pp.\ 40--51, 1992.
-
-\nbibitem[Mitc08]{catch}{}{}{}
-N.~Mitchell and C.~Runciman,
-\newblock ``Not All Patterns, But Enough - an automatic verifier for partial
-  but sufficient pattern matching'',
-\newblock in {\em Haskell}, 2008.
-
-\nbibitem[Nels81]{Nelson81}{}{}{}
-G.~Nelson,
-\newblock ``Techniques for program verification'',
-\newblock Technical Report CSL81-10, Xerox Palo Alto Research Center, 1981.
-
-\nbibitem[Nipk02]{NPW2002}{}{}{}
-T.~Nipkow, L.C. Paulson and M.~Wenzel,
-\newblock {\em {Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
-  vol.\ 2283 of {\em Lecture Notes in Computer Science},
-\newblock Springer, 2002.
-
-\nbibitem[Nore07]{norell07}{}{}{}
-U.~Norell,
-\newblock {\em Towards a practical programming language based on dependent type
-  theory},
-\newblock Ph.D.\ thesis, Chalmers, 2007.
-
-\nbibitem[Ou04]{Ou2004}{}{}{}
-X.~Ou, G.~Tan, Y.~Mandelbaum and D.~Walker,
-\newblock ``Dynamic Typing with Dependent Types'',
-\newblock in {\em IFIP TCS}, 2004.
-
-\nbibitem[Pugh92]{OmegaTestCACM}{}{}{}
-W.~Pugh,
-\newblock ``A practical algorithm for exact array dependence analysis'',
-\newblock {\em Communications of the ACM}, vol.~35, no.~8, pp.\ 102--114,
-  August 1992.
-
-\nbibitem[Rond08]{LiquidPLDI08}{}{}{}
-P.~Rondon, M.~Kawaguchi and R.~Jhala,
-\newblock ``Liquid Types'',
-\newblock in {\em PLDI}, 2008.
-
-\nbibitem[Rond10]{Rondon10}{}{}{}
-Patrick~Maxim Rondon, Ming Kawaguchi and Ranjit Jhala,
-\newblock ``Low-level liquid types'',
-\newblock in {\em POPL}, pp.\ 131--144, 2010.
-
-\nbibitem[Sulz07]{SulzmannCJD07}{}{}{}
-M.~Sulzmann, M.~M.~T. Chakravarty, S.~L. Peyton-Jones and K.~Donnelly,
-\newblock ``System {F} with type equality coercions'',
-\newblock in {\em TLDI}, 2007.
-
-\nbibitem[Sute11]{SuterKK11}{}{}{}
-Philippe Suter, Ali~Sinan K{\"o}ksal and Viktor Kuncak,
-\newblock ``Satisfiability Modulo Recursive Programs'',
-\newblock in {\em SAS}, pp.\ 298--315, 2011.
-
-\nbibitem[Swam11]{SwamyCFSBY11}{}{}{}
-N.~Swamy, J.~Chen, C.~Fournet, P-Y. Strub, K.~Bhargavan and J.~Yang,
-\newblock ``Secure distributed programming with value-dependent types'',
-\newblock in {\em ICFP}, pp.\ 266--278, 2011.
-
-\nbibitem[Swie12]{Swierstra2012}{}{}{}
-W.~Swierstra,
-\newblock ``Xmonad in {Coq} (experience report): Programming a Window Manager
-  In A Proof Assistant'',
-\newblock in {\em Haskell Symposium}, 2012.
-
-\nbibitem[Tobi08]{Tobin-HochstadtF08}{}{}{}
-Sam Tobin-Hochstadt and Matthias Felleisen,
-\newblock ``The design and implementation of typed scheme'',
-\newblock in {\em POPL}, pp.\ 395--406, 2008.
-
-\nbibitem[Unno13]{UnnoTK13}{}{}{}
-Hiroshi Unno, Tachio Terauchi and Naoki Kobayashi,
-\newblock ``Automating relatively complete verification of higher-order
-  functional programs'',
-\newblock in {\em POPL}, pp.\ 75--86, 2013.
-
-\nbibitem[Vazo13]{Vazou13}{}{}{}
-N.~Vazou, P.~Rondon and R.~Jhala,
-\newblock ``Abstract Refinement Types'',
-\newblock in {\em ESOP}, 2013.
-
-\nbibitem[Vazo14]{LiquidICFP14}{}{}{}
-N.~Vazou, E.~L. Seidel, R.~Jhala, D.~Vytiniotis and S.~Peyton-Jones,
-\newblock ``Refinement Types for Haskell'',
-\newblock in {\em ICFP}, 2014.
-
-\nbibitem[Vyti13]{VytiniotisJCR13}{}{}{}
-Dimitrios Vytiniotis, Simon L.~Peyton Jones, Koen Claessen and Dan Ros{\'e}n,
-\newblock ``HALO: haskell to logic through denotational semantics'',
-\newblock in {\em POPL}, pp.\ 431--442, 2013.
-
-\nbibitem[Wadl09]{WadlerF09}{}{}{}
-Philip Wadler and Robert~Bruce Findler,
-\newblock ``Well-Typed Programs Can't Be Blamed'',
-\newblock in {\em ESOP}, pp.\ 1--16, 2009.
-
-\nbibitem[Xi98]{pfenningxi98}{}{}{}
-H.~Xi and F.~Pfenning,
-\newblock ``Eliminating Array Bound Checking Through Dependent Types.'',
-\newblock in {\em PLDI}, 1998.
-
-\nbibitem[Xi99]{XiPfenning99}{}{}{}
-H.~Xi and F.~Pfenning,
-\newblock ``Dependent Types in Practical Programming'',
-\newblock in {\em POPL}, 1999.
-
-\nbibitem[Xi01]{XiTerminationLICS01}{}{}{}
-H.~Xi,
-\newblock ``Dependent Types for Program Termination Verification'',
-\newblock in {\em LICS}, 2001.
-
-\end{thebibliography}

test.bib

-@article{church-1932-spfl,
-  author="A. Church",
-  title="A Set of Postulates for the Foundations of Logic",
-  journal="Annals of Mathematics",
-  volume=33,
-  pages="346--366",
-  number=1,
-  year=1932
-}
-
-@article{church-1933-spfl,
-  author="A. Church",
-  title="A Set of Postulates for the Foundations of Logic",
-  journal="Annals of Mathematics",
-  volume=34,
-  pages="839--864",
-  number=2,
-  year=1933
-}
-  
-@phdthesis{girard-1972-ifecaos,
-  author="J.-Y. Girard",
-  title="Interpr{\'e}tation Fonctionelle et {\'E}limination des "
-       # "Coupures Dans l'Arithm{\'e}tique d'Ordre Sup{\'e}rieur",
-  school="Universit{\'e} Paris 7",
-  year=1972
-}
-
-@article{girard-1989-pt,
-  author="J.-Y. Girard and Y. Lafont and P. Taylor",
-  title="Proofs and Types",
-  journal="Tracks in Theoretical Computer Science",
-  year=1989
-}
-
-@inproceedings{reynolds-1974-ttts,
-  author="John. C. Reynolds",
-  title="Towards a Theory of Type Systems",
-  booktitle="Lecture Notes in Computer Science",
-  year=1974,
-  editor="Ehring et al.",
-  volume=19,
-  pages="408--425",
-  publisher="Springer-Verlag"
-}
-
-@article{boehm-1985-astlpta,
-  author="C. B{\"o}hm and A. Bernarducci",
-  title="Automatic Synthesis of Typed $\lambda$-Programs on Term "
-       # "Algebras",
-  journal="Theoretical Computer Science",
-  volume=39,
-  number="2--3",
-  pages="135--154",
-  month=aug,
-  year=1985
-}
-
-@phdthesis{paulin-1989-epscc,
-  author="C. Paulin-Mohring",
-  title="Extraction de Programmes Dans le Calcul des Constructions",
-  month=jan,
-  school="Universit{\'e} Paris 7",
-  year=1989,
-  url="http://www.lri.fr/~paulin/these.ps.gz"
-}
-
-@inproceedings{pfenning-1990-pmfps,
-  author="F. Pfenning and C. Paulin-Mohring",
-  booktitle="Proceedings of Mathematical Foundations of "
-           # "Programming Semantics",
-  note="technical report CMU-CS-89-209",
-  publisher="Springer-Verlag",
-  address = "Berlin",
-  series="Lecture Notes in Computer Science",
-  volume=442,
-  title="Inductively defined types in the Calculus of Constructions",
-  year=1990
-}
-
-@incollection{paulin-1993-iddcrp,
-  author= "Christine Paulin-Mohring",
-  title = "Inductive Definitions in the System {Coq}: Rules and Properties",
-  booktitle = "Proceedings of the 1st Int.\ Conf.\ on Typed Lambda Calculi "
-           # "and Applications, {TLCA}'93, Utrecht, The Netherlands, "
-	   # "16--18 March 1993",
-  volume = 664,
-  publisher = "Springer-Verlag",
-  address = "Berlin",
-  editor = "M. Bezem and J. F. Groote",
-  pages = "328--345",
-  year = 1993,
-  url = "citeseer.nj.nec.com/paulin-mohring92inductive.html"
-}
-
-@InProceedings{shao-2002-tscb,
-  author = 	 "Z. Shao and B. Saha and V. Trifonov and N. Papaspyrou",
-  title = 	 "A Type System for Certified Binaries",
-  booktitle = 	 "Proceedings of the 29th Annual Symposium on Principles of "
-               # "Programming Languages (POPL 2002)",
-  year =	 2002,
-  pages =	 "217--232",
-  address =	 "Portland, OR, USA",
-  month =	 jan
-}
-
-@InProceedings{sellink-1994-vpaptt,
-  author = 	 "M. P. A. Sellink",
-  title = 	 "Verifying process algebra proofs in type theory",
-  booktitle = 	 "Proceedings of the International Workshop on Semantics "
-               # " of Specipication Languages (SOSL 1993)",
-  year =	 1994,
-  editor =	"D. J. Andrews and J. F. Groote and C. A. Middelburg",
-  publisher = 	"Springer"
-}
-
-@inproceedings{necula-1997-pcc,
-  author="G. Necula",
-  title="Proof-Carrying Code",
-  booktitle="Proceedings of the 24th Annual Symposium on Principles of "
-           # "Programming Languages (POPL 1997)",
-  pages="106--119",
-  publisher="ACM Press",
-  address="New York",
-  year=1997,
-  month=jan
-}
-
-@inproceedings{necula-1996-skertc,
-  author="G. Necula and P. Lee",
-  title="Safe Kernel Extensions without Run-Time Checking",
-  booktitle="Proceedings of the 2nd USENIX Symposium on Operating "
-	# "System Design and Implementation", 
-  year="1996",
-  publisher="USENIX Association",
-  pages="229--243"
-}
-
-@phdthesis{necula-1998-cp,
-  title = "Compiling with Proofs",
-  author = "G. Necula",
-  school = "Carnegie Mellon University",
-  year = 1998,
-  month=sep,
-  number = "CMU-CS-98-154"
-}
-
-@inproceedings{appel-2000-smtmipcc,
-  author="Andrew W. Appel and Amy P. Felty",
-  title="A Semantic Model of Types and Machine Instructions for "
-	# "Proof-Carrying Code",
-  booktitle="Proceedings of the 27th Annual Symposium on Principles of "
-           # "Programming Languages (POPL 2000)",
-  year=2000,
-  publisher = "ACM Press",
-  pages="243--253"
-}
-
-@InProceedings{appel-2001-fpcc,
-  author = 	 "A. W. Appel",
-  title = 	 "Foundational Proof-Carrying Code",
-  booktitle = 	 "Proceedings of the 16th Annual IEEE Symposium on "
-	       # "Logic in Computer Science",
-  pages =	 "247--258",
-  year =	 2001,
-  month =	 jun
-}
-
-@inproceedings{harper-1995-cpita,
-  author="Robert Harper and Greg Morrisett",
-  title="Compiling Polymorphism Using Intensional Type Analysis",
-  booktitle="Proceedings of the 22nd Annual Symposium on Principles of "
-           # "Programming Languages (POPL 1995)",
-  publisher="ACM Press",
-  year="1995",
-  pages="130--141"
-}
-
-@inproceedings{morrisett-1998-sftal,
-  author="Greg Morrisett and David Walker and Karl Crary and Neal Glew",
-  title="From {S}ystem {F} to Typed Assembly Language",
-  booktitle="Proceedings of the 25th Annual Symposium on Principles of "
-           # "Programming Languages (POPL 1998)",
-  pages="85--97",
-  publisher="ACM Press",
-  year=1998,
-  month=jan
-}

test.blg

-This is BibTeX, Version 0.99d (TeX Live 2014)
-Capacity: max_strings=35307, hash_size=35307, hash_prime=30011
-The top-level auxiliary file: test.aux
-Case mismatch error between cite keys Z3 and z3
----line 158 of file test.aux
- : \citation{Z3
- :             }
-I'm skipping whatever remains of this command
-Case mismatch error between cite keys vazou13 and Vazou13
----line 178 of file test.aux
- : \citation{vazou13
- :                  }
-I'm skipping whatever remains of this command
-Case mismatch error between cite keys vazou13 and Vazou13
----line 188 of file test.aux
- : \citation{vazou13
- :                  }
-I'm skipping whatever remains of this command
-Case mismatch error between cite keys vazou13 and Vazou13
----line 199 of file test.aux
- : \citation{vazou13
- :                  }
-I'm skipping whatever remains of this command
-Case mismatch error between cite keys Z3 and z3
----line 210 of file test.aux
- : \citation{Z3
- :             }
-I'm skipping whatever remains of this command
-The style file: softlab-thesis.bst
-Database file #1: sw.bib
-Repeated entry---line 17521 of file sw.bib
- : @book{    Constable86
- :                      ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 18621 of file sw.bib
- : @book{    Eiffel
- :                 ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19104 of file sw.bib
- : @inproceedings{   Findler02
- :                            ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19164 of file sw.bib
- : @inproceedings{   flanagan06
- :                             ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19412 of file sw.bib
- : @inproceedings{   LiquidPLDI08
- :                               ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19419 of file sw.bib
- : @inproceedings{   LiquidPLDI09
- :                               ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19503 of file sw.bib
- : @inproceedings{cayenne
- :                       ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19793 of file sw.bib
- : @inproceedings{Greenberg11
- :                           ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19806 of file sw.bib
- : @inproceedings{Vazou13
- :                       ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19815 of file sw.bib
- : @inproceedings{vazou13
- :                       ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19825 of file sw.bib
- : @article{Greenberg12
- :                     ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 19853 of file sw.bib
- : @inproceedings{Gronski06
- :                         ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 23320 of file sw.bib
- : @inproceedings{  MandelbaumWalker03
- :                                    ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 23361 of file sw.bib
- : @article{   Meyer92
- :                    ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 23893 of file sw.bib
- : @techreport{   Nelson81
- :                        ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 23992 of file sw.bib
- : @phdthesis{norell07
- :                    ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 24001 of file sw.bib
- : @book{    NPW2002
- :                  ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 24090 of file sw.bib
- : @article{   OmegaTestCACM
- :                          ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 25662 of file sw.bib
- : @inproceedings{z3
- :                  ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 25670 of file sw.bib
- : @inproceedings{Z3
- :                  ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 25678 of file sw.bib
- : @unpublished{    Yices
- :                       ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 27015 of file sw.bib
- : @inproceedings{pfenningxi98
- :                            ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 27032 of file sw.bib
- : @inproceedings{XiPfenning99
- :                            ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 27384 of file sw.bib
- : @inproceedings{ Ou2004
- :                       ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 27718 of file sw.bib
- : @inproceedings{dminor
- :                      ,
-I'm skipping whatever remains of this entry
-Repeated entry---line 27980 of file sw.bib
- : @book{coq-book
- :               ,
-I'm skipping whatever remains of this entry
-Warning--to sort, need author, editor, or key in cpdt
-"" isn't a single character for entry SMTLIB2
-while executing---line 1858 of file softlab-thesis.bst
-Warning--empty booktitle in SMTLIB2
-"" isn't a single character for entry cpdt
-while executing---line 1858 of file softlab-thesis.bst
-Warning--empty author and editor in cpdt
-"" isn't a single character for entry z3
-while executing---line 1858 of file softlab-thesis.bst
-Warning--empty journal in z3
-You've used 50 entries,
-            2802 wiz_defined-function locations,
-            876 strings with 10331 characters,
-and the built_in function-call counts, 42241 in all, are:
-= -- 5133
-> -- 2465
-< -- 68
-+ -- 269
-- -- 264
-* -- 3117
-:= -- 6416
-add.period$ -- 50
-call.type$ -- 50
-change.case$ -- 281
-chr.to.int$ -- 91
-cite$ -- 55
-duplicate$ -- 1133
-empty$ -- 1790
-format.name$ -- 313
-if$ -- 7632
-int.to.chr$ -- 1
-int.to.str$ -- 0
-missing$ -- 50
-newline$ -- 253
-num.names$ -- 100
-pop$ -- 610
-preamble$ -- 1
-purify$ -- 430
-quote$ -- 0
-skip$ -- 716
-stack$ -- 0
-substring$ -- 7482
-swap$ -- 201
-text.length$ -- 1731
-text.prefix$ -- 50
-top$ -- 0
-type$ -- 380
-warning$ -- 4
-while$ -- 281
-width$ -- 53
-write$ -- 771
-(There were 34 error messages)

test.toc

-\select@language {greek}
-\select@language {greek}
-\contentsline {chapter}{Περίληψη}{5}
-\select@language {greek}
-\select@language {english}
-\contentsline {chapter}{Abstract}{7}
-\select@language {greek}
-\select@language {greek}
-\contentsline {chapter}{Ευχαριστίες}{9}
-\select@language {greek}
-\contentsline {chapter}{Περιεχόμενα}{11}
-\addvspace {1em}
-\contentsline {chapter}{\numberline {1.}Introduction}{13}
-\contentsline {chapter}{\numberline {2.}Preliminaries}{15}
-\contentsline {section}{\numberline {2.1}Syntax}{15}
-\contentsline {section}{\numberline {2.2}Typing}{15}
-\contentsline {chapter}{\numberline {3.}Undecidable Systems}{17}
-\contentsline {section}{\numberline {3.1}Interactive theorem Proving}{17}
-\contentsline {section}{\numberline {3.2}Contracts}{18}
-\contentsline {subsection}{\numberline {3.2.1}Manifest Contracts}{19}
-\contentsline {subsection}{\numberline {3.2.2}Formal Language}{20}
-\contentsline {chapter}{\numberline {4.}Decidable Type Systems}{21}
-\contentsline {section}{\numberline {4.1}Liquid Types}{22}
-\contentsline {subsection}{\numberline {4.1.1}Applications of Liquid Types}{23}
-\contentsline {subsection}{\numberline {4.1.2}Formal Language}{24}
-\contentsline {chapter}{\numberline {5.}Abstract Refinement Types}{25}
-\contentsline {section}{\numberline {5.1}The key idea}{25}
-\contentsline {section}{\numberline {5.2}Inductive Refinements}{26}
-\contentsline {section}{\numberline {5.3}Function Composition}{27}
-\contentsline {section}{\numberline {5.4}Index-Dependent Invariants}{28}
-\contentsline {section}{\numberline {5.5}Recursive Invariants}{28}
-\contentsline {section}{\numberline {5.6}Formal Language}{29}
-\contentsline {chapter}{\numberline {6.}\textsc {LiquidHaskell}\xspace }{31}
-\contentsline {subsection}{\numberline {6.0.1}Specifications}{32}
-\contentsline {subsection}{\numberline {6.0.2}Verification}{32}
-\contentsline {subsection}{\numberline {6.0.3}Measures}{33}
-\contentsline {subsection}{\numberline {6.0.4}Refined Data Types}{34}
-\contentsline {subsection}{\numberline {6.0.5}Refined Type Classes}{35}
-\contentsline {subsection}{\numberline {6.0.6}Abstracting Refinements}{36}
-\contentsline {chapter}{\numberline {7.}Totality}{39}
-\contentsline {subsection}{\numberline {7.0.7}Specifying Totality}{39}
-\contentsline {subsection}{\numberline {7.0.8}Verifying Totality}{39}
-\contentsline {subsection}{\numberline {7.0.9}Case Studies}{40}
-\contentsline {chapter}{\numberline {8.}Termination}{43}
-\contentsline {chapter}{\numberline {9.}Functional Correctness Invariants}{47}
-\contentsline {subsection}{\numberline {9.0.10}Red-Black Trees}{47}
-\contentsline {subsection}{\numberline {9.0.11}Stack Sets in XMonad}{48}
-\contentsline {chapter}{\numberline {10.}Conclusion}{53}
-\addvspace {1em}
-\contentsline {chapter}{Βιβλιογραφία}{55}
-\addvspace {1em}

test.tex → thesis.tex

- \documentclass[diploma]{softlab-thesis}
-
-\usepackage{amsmath,amssymb, latexsym}
+\documentclass[mpla]{softlab-thesis}
 
 \usepackage{amsmath}
 \usepackage{amsfonts}
 \usepackage{amssymb}
+\usepackage{latexsym}
 
 \usepackage{liquidHaskell}
 \usepackage[inference]{semantic}
@@ -58,8 +57,8 @@
 
 \title{LiquidHaskell : Liquid Types for Haskell}
 \author{Νίκη Βάζου}
-\date{Γενάρης 2015}
-\datedefense{8}{1}{2015}
+\date{Απρίλιος 2015}%{Γενάρης 2015}
+\datedefense{3}{4}{2015}%{8}{1}{2015}
 
 \supervisor{Νικόλαος Σ. Παπασπύρου}
 \supervisorpos{Αν. Καθηγητής Ε.Μ.Π.}
@@ -71,8 +70,7 @@
 \committeethree{Παναγιώτης Ροντογιάννης}
 \committeethreepos{Αν. Καθηγητής  Ε.Κ.Π.Α.}
 
-\TRnumber{CSD-SW-TR-42-14}  % number-year, ask nickie for the number
-\department{Τομέας Τεχνολογίας Πληροφορικής και Υπολογιστών}
+\TRnumber{CSD-SW-TR-2-15}  % number-year, ask nickie for the number
 
 \maketitle
 
@@ -151,6 +149,9 @@ Refinement Types, Abstract Interpretation, Algorithmic Verification
 \end{acknowledgementsgr}
 
 
+\selectlanguage{english}   % Everything from here on is in english
+
+
 %%%  Various tables
 
 \tableofcontents

tool.tex

@@ -85,7 +85,7 @@ compatibility with existing compilers, all specifications
 appear within comments of the form \verb|{-@ ... @-}|, 
 which we omit below for brevity.
 
-\subsection{Specifications}
+\section{Specifications}
 
 A refinement type is a Haskell type where each component
 of the type is decorated with a predicate from a (decidable)
@@ -144,7 +144,7 @@ Third, the refinement in the \emph{output} type describes the
 the bounds of @lo@ and @hi@.
 
 
-\subsection{Verification}\label{sec:tool:verification}
+\section{Verification}\label{sec:tool:verification}
 
 Next, consider the following implementation for @range@:
 %
@@ -218,7 +218,7 @@ the system defaults to using the trivial (unrefined) Haskell
 type as the signature \ie, checks the implementation assuming 
 arbitrary inputs.
 
-\subsection{Measures}\label{sec:tool:measures}
+\section{Measures}\label{sec:tool:measures}
 %% \NV{DONE(R1)
 %% measure is introduced as something that gives the size of a value, 
 %% but it is later used for more general properties e.g. almostRB 
@@ -312,7 +312,7 @@ but will reject
 
 
 
-\subsection{Refined Data Types}
+\section{Refined Data Types}
 
 Often, we require that \emph{every} instance of a type satisfies some invariants. 
 For example, consider a @CSV@ data type, that represents tables:
@@ -364,7 +364,7 @@ are well-typed Haskell, but the latter is rejected by \toolname.
 Like measures, the global invariants are enforced by refining 
 the constructors' types. 
 
-\subsection{Refined Type Classes}\label{sec:type-classes}
+\section{Refined Type Classes}\label{sec:type-classes}
 
 Next, let us see how \toolname supports the verification of
 programs that use ad-hoc polymorphism via type classes.
@@ -449,7 +449,7 @@ Specifically, each call to @at@ is guarded by a check @i < size xs@
 and @i@ is  increasing 
 from 0, so \toolname proves that @xs `at` i@ will always be safe.
 
-\subsection{Abstracting Refinements}
+\section{Abstracting Refinements}
 
 So far, all the specifications have used \emph{concrete} refinements. Often it is
 useful to be able to \emph{abstract} the refinements that appear in a
@@ -474,7 +474,7 @@ We would like to give @max@ a specification that lets us verify:
 \end{code}
 %
 To this end, \toolname allows the user to \emph{abstract refinements} over
-types~\cite{vazou13}, for example by typing @max@ as:
+types~\cite{Vazou13}, for example by typing @max@ as:
 %
 \begin{code}
  max :: forall <p :: Int -> Prop>. 

totality.tex

@@ -13,7 +13,7 @@ As our first application, let us see how to use
 of such exceptions, \ie, to prove various 
 functions \emph{total}.
 
-\subsection{Specifying Totality}
+\section{Specifying Totality}
 
 First, let us see how to specify the notion of
 totality inside \toolname. Consider the source of 
@@ -55,7 +55,7 @@ and so an expression containing a call to @patError@ will only type
 check if the call is \emph{dead code}.
 
 
-\subsection{Verifying Totality}
+\section{Verifying Totality}
 
 The (core) definition of @head@ does not typecheck
 as is; but requires a pre-condition that states that the function
@@ -159,7 +159,7 @@ by invoking \toolname with the \cmdtotality command line option,
 at which point the tool systematically checks that all the above 
 functions are indeed dead code, and hence, that all definitions are total.
 
-\subsection{Case Studies}
+\section{Case Studies}
 
 We verified totality of two libraries: \lbhscolour and \lbmap, earlier versions
 of which had previously been proven total by \texttt{catch}~\citep{catch}.
@@ -169,7 +169,7 @@ is a widely used library for (immutable) key-value maps, implemented
 as balanced binary search trees.
 Totality verification of \lbmap was quite straightforward.
 We had previously verified termination and the crucial 
-binary search invariant~\citep{vazou13}. To verify 
+binary search invariant~\citep{Vazou13}. To verify 
 totality it sufficed to simply re-run verification with
 the \cmdtotality argument.
 %
@@ -185,7 +185,7 @@ and no additional changes were needed to prove totality.
 %
 
 This case study illustrates an advantage of \toolname over specialized provers 
-(\eg, \texttt{catch}~\citep{catch}), namely it can be used to prove totality, termination and
+(\eg, \texttt{catch} \citep{catch}), namely it can be used to prove totality, termination and
 functional correctness at the same time, facilitating a nice reuse of
 specifications for multiple tasks.
 

undecidable.tex

@@ -417,7 +417,7 @@ $$
 \end{array}
 $$
 \caption{\textbf{Syntax} from $\lambda_C$ to $\lambda_{CC}$}
-\label{fig:syntax}
+\label{fig:syntax2}
 \end{figure}
 
 
@@ -460,7 +460,7 @@ $$\begin{array}{cc}
 
 
 \caption{\textbf{Static Semantics} from $\lambda_C$ to $\lambda_{CC}$}
-\label{fig:rules}
+\label{fig:rules3}
 \end{figure}
 
 \begin{comment}
@@ -553,7 +553,7 @@ $$\begin{array}{cc}
 \end{array}$$
 
 \caption{\textbf{Static Semantics} from $\lambda_{CC}$ to $\lambda_{CH}$}
-\label{fig:rules}
+\label{fig:rules4}
 \end{figure}
 \end{comment}