draft is ready

Makefile

@@ -17,3 +17,6 @@ clean:
 
 distclean: clean
 	$(RM) $(FILE).{dvi,ps,pdf}
+
+
+

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
+

TODO.md

+* Introduction [1/2pp]
+
+  1. What kind of things do you check?
+
+  2. How do you use it?
+     * what does the user provide?
+     * what feedback do you get etc?
+
+  3. What are the limitations?
+
+* Termination [1 1/2 pp, DONE]
+  * Mutual Recursive Functions
+  * GHCSort
+
+* Totality Checker [1 1.2pp, DONE]
+  * hscolour, Data.Map
+
+* Memory Safety [3pp, E]
+   * ByteString
+   * Text
+   * Vector-Algos
+
+* Interesting Specifications [1-2pp, NV HERE]
+  * XMONAD
+  * Red Black Tree
+
+* Results [1pp, E]
+  * Benchmark Statistics
+
+* Discussion [1pp, E]
+  * Code Changes
+  * Limitations
+
+* Related Work [1/2pp]
+
+* [ ] XMonad (??)
+
+
+points to cover:
+
+  measure, 
+  abstract refinement, 
+  type holes, 

abstract.tex

+Even well-typed programs can go wrong,
+by returning a wrong answer or 
+throwing a run-time error.
+A popular response is
+to allow programmers use
+\textit{refinement type systems}
+to express semantic specifications 
+about programs.
+%
+We study verification in such systems.
+%
+On the one hand, expressive refinement type systems
+require run-time checks
+or explicit proofs to verify specifications.
+On the other,
+less expressive type systems
+allow static and automatic proofs of the specifications.
+%
+Next, we present abstract refinement types, 
+a means to enhance the expressiveness of
+a refinement type system without increasing its complexity.
+Then,  we present \toolname
+that combines liquidTypes with abstraction over refinements
+to enhance expressiveness of LiquidTypes.
+\toolname is a quite expressive verification tool for Haskell programs 
+that can be used to check termination, 
+totality  and general functional correctness.
+Finally, we evaluate \toolname in real world Haskell libraries.
\ No newline at end of file

bytestring.tex

+% The terms ``Haskell'' and ``pointer arithmetic'' 
+% rarely occur in the same sentence. 
+% Thus, from a verification point of view, the 
+The single most important aspect of the \bytestring 
+library,%~\cite{bytestring}, 
+our first case study, is its pervasive intermingling of
+high level abstractions like higher-order loops,
+folds, and fusion, with low-level pointer 
+manipulations in order to achieve high-performance. 
+%
+%% From the package description, \bytestring is, 
+%% ``A time and space-efficient implementation of byte vectors using packed
+%% Word8 arrays, suitable for high performance use, both in terms of large
+%% data quantities, or high speed requirements. Byte vectors are encoded as
+%% strict Word8 arrays of bytes, held in a ForeignPtr, and can be passed
+%% between C and Haskell with little effort."
+%
+\bytestring is an appealing target for evaluating
+\toolname, as refinement types are an ideal way to 
+statically ensure the correctness of the delicate 
+pointer manipulations, errors in which lie below 
+the scope of dynamic protection.
+
+The library spans $8$ files (modules) totaling about 3,500 lines.
+We used \toolname to verify the library by giving precise 
+types describing the sizes of internal pointers and bytestrings. 
+These types are used in a modular fashion to verify the 
+implementation of functional correctness properties of 
+higher-level API functions which are built using 
+lower-level internal operations. 
+Next, we show the key invariants and how
+\toolname reasons precisely about pointer
+arithmetic and higher-order codes.
+
+\spara{Key Invariants}
+A (strict) @ByteString@ is a triple of a @pay@load pointer, 
+an @off@set into the memory buffer referred to by the pointer 
+(at which the string actually ``begins") and a @len@gth 
+corresponding to the number of bytes in the string, which is 
+the size of the buffer \emph{after} the @off@set, that
+corresponds to the string.
+%
+We define a measure for the \emph{size} of 
+a @ForeignPtr@'s buffer, and use it to define 
+the key invariants as a refined datatype 
+%
+\begin{code}
+  measure fplen  :: ForeignPtr a -> Int
+  data ByteString = PS
+   { pay :: ForeignPtr Word8
+   , off :: {v:Nat | v       <= (fplen pay)}
+   , len :: {v:Nat | off + v <= (fplen pay)} }
+\end{code}
+%
+The definition states that 
+the offset is a @Nat@ no bigger than the size of 
+the @payload@'s buffer, and that
+the sum of the @off@set and non-negative @len@gth
+is no more than the size of the payload buffer.
+Finally, we encode a @ByteString@'s size as a measure.
+%
+\begin{code}
+  measure bLen   :: ByteString -> Int
+  bLen (PS p o l) = l
+\end{code}
+
+\spara{Specifications}
+We define a type alias for a @ByteString@ whose length is the same
+as that of another, and use the alias to type the API 
+function @copy@, which clones @ByteString@s.
+
+\begin{code}
+  type ByteStringEq B 
+    = {v:ByteString | (bLen v) = (bLen B)}
+  copy :: b:ByteString -> ByteStringEq b 
+  copy (PS fp off len) 
+    = unsafeCreate len $ \p -> 
+        withForeignPtr fp $ \f ->
+          memcpy len p (f `plusPtr` off) 
+\end{code}
+
+\spara{Pointer Arithmetic}
+The simple body of @copy@ abstracts a fair bit of internal work. 
+@memcpy sz dst src@, implemented in \C and accessed via the FFI is a potentially
+dangerous, low-level operation, that copies @sz@ bytes starting
+\emph{from} an address @src@ \emph{into} an address @dst@. 
+Crucially, for safety, the regions referred to be @src@ and @dst@ 
+must be larger than @sz@. We capture this requirement by defining
+a type alias @PtrN a N@ denoting GHC pointers that refer to a region
+bigger than @N@ bytes, and then specifying that the destination
+and source buffers for @memcpy@ are large enough. 
+
+\begin{code}
+  type PtrN a N = {v:Ptr a | N <= (plen v)}
+  memcpy :: sz:CSize -> dst:PtrN a siz 
+                     -> src:PtrN a siz 
+                     -> IO () 
+\end{code}
+
+
+The actual output for @copy@ is created and filled in using the 
+internal function @unsafeCreate@ which is a wrapper around. 
+% -- | Create ByteString of size @l@ and use
+% --   action @f@ to fill it's contents.
+\begin{code}
+  create :: l:Nat -> f:(PtrN Word8 l -> IO ())
+         -> IO (ByteStringN l)
+  create l f = do
+      fp <- mallocByteString l
+      withForeignPtr fp $ \p -> f p
+      return $! PS fp 0 l
+\end{code}
+
+% We include the comment to illustrate how the 
+% refinement type captures the natural language 
+% requirement in a machine checkable manner.
+%
+The type of @f@ specifies that the action
+will only be invoked on a pointer of length at least 
+@l@, which is verified by propagating the types of
+@mallocByteString@ and @withForeignPtr@. 
+%
+The fact that the action is only invoked on such pointers 
+is used to ensure that the value @p@ in the body of @copy@ 
+is of size @l@. This, and the @ByteString@ 
+invariant that the size of the payload @fp@ 
+exceeds the sum of @off@ and @len@, ensures 
+that the call to @memcpy@ is safe.
+
+\spara{Interfacing with the Real World}
+The above illustrates how \toolname analyzes code that interfaces 
+with the ``real world" via the \C FFI. We specify the behavior 
+of the world via a refinement typed interface. These types are then assumed
+to hold for the corresponding functions, \ie generate pre-condition checks
+and post-condition guarantees at usage sites within the Haskell code.
+
+
+\spara{Higher Order Loops} 
+@mapAccumR@ combines a @map@ and a @foldr@ over a @ByteString@. 
+The function uses non-trivial recursion, and demonstrates 
+the utility of abstract-interpretation based inference. 
+%
+\begin{code}
+  mapAccumR f z b 
+    = unSP $ loopDown (mapAccumEFL f) z b
+\end{code}
+%$
+To enable fusion \cite{streamfusion} 
+@loopDown@ uses a higher order @loopWrapper@ 
+to iterate over the buffer with a @doDownLoop@ action:
+%
+%% DONE \ES{should we use a termination expression for ``loop'' even though it won't actually work atm in LH?}
+\begin{code}
+  doDownLoop f acc0 src dest len 
+    = loop (len-1) (len-1) acc0
+    where
+     loop :: s:_ -> _ -> _ -> _ / [s+1]
+     loop s d acc
+       | s < 0 
+       = return (acc :*: d+1 :*: len - (d+1))
+       | otherwise       
+       = do x <- peekByteOff src s
+            case f acc x of
+              (acc' :*: NothingS) -> 
+                   loop (s-1) d acc'
+              (acc' :*: JustS x') -> 
+                   pokeByteOff dest d x'
+                >> loop (s-1) (d-1) acc'
+\end{code}
+
+The above function iterates across the @src@ and @dst@ 
+pointers from the right (by repeatedly decrementing the 
+offsets @s@ and @d@ starting at the high @len@ down to @-1@). 
+Low-level reads and writes are carried out using the 
+potentially dangerous @peekByteOff@ and @pokeByteOff@ 
+respectively. To ensure safety, we type these low level 
+operations with refinements stating that they are only 
+invoked with valid offsets @VO@ into the input buffer @p@.
+
+\begin{code}
+  type VO P    = {v:Nat | v < plen P}
+  peekByteOff :: p:Ptr b -> VO p -> IO a
+  pokeByteOff :: p:Ptr b -> VO p -> a -> IO ()
+\end{code}
+
+The function @doDownLoop@ is an internal function.
+Via abstract interpretation~\cite{LiquidPLDI08}, 
+\toolname infers that
+%
+(1)~@len@ is less than the sizes of @src@ and @dest@,
+(2)~@f@ (here, @mapAccumEFL@) always returns a @JustS@, so
+(3)~source and destination offsets satisfy $\mathtt{0 \leq s, d < {len}}$,
+(4)~the generated @IO@ action returns a triple @(acc :*: 0 :*: len)@,
+%
+thereby proving the safety of the accesses in @loop@ \emph{and}
+verifying that @loopDown@ and the API function @mapAccumR@ 
+return a \bytestring whose size equals its input's.
+ 
+To prove \emph{termination}, we add a \emph{termination expression} 
+@s+1@ which is always non-negative and decreases at each call.
+
+\spara{Nested Data}
+@group@ splits a string like @"aart"@ into the list
+@["aa","r","t"]@, \ie a list of
+(a)~non-empty @ByteString@s whose 
+(b)~total length equals that of the input. 
+To specify these requirements, we define a measure for 
+the total length of strings in a list and use it to
+write an alias for a list of \emph{non-empty} strings
+whose total length equals that of another string:
+
+\begin{code}
+  measure bLens :: [ByteString] -> Int 
+  bLens ([])     = 0
+  bLens (x:xs)   = bLen x + bLens xs
+  
+  type ByteStringNE 
+    = {v:ByteString | bLen v > 0}
+  type ByteStringsEq B
+    = {v:[ByteStringNE] | bLens v = bLen b}
+\end{code}
+%
+\toolname uses the above to verify that
+%
+\begin{code}
+  group :: b:ByteString -> ByteStringsEq b
+  group xs
+   | null xs   = []
+   | otherwise = let x        = unsafeHead xs
+                     xs'      = unsafeTail xs
+                     (ys, zs) = spanByte x xs' 
+                 in (y `cons` ys) : group zs
+\end{code}
+%
+The example illustrates why refinements are critical for
+proving termination. \toolname determines that @unsafeTail@ 
+returns a \emph{smaller} @ByteString@ than its input, and that
+each element returned by @spanByte@ is no bigger than the 
+input, concluding that @zs@ is smaller than @xs@, and hence
+checking the body under the termination-weakened environment.
+
+To see why the output type holds, let's look at @spanByte@,
+which splits strings into a pair:
+%
+\begin{code}
+  spanByte c ps@(PS x s l) 
+    = inlinePerformIO $ withForeignPtr x $
+          \p -> go (p `plusPtr` s) 0
+    where
+      go :: _ -> i:_ -> _ / [l-i]
+      go p i 
+        | i >= l    = return (ps, empty)
+        | otherwise = do
+            c' <- peekByteOff p i
+            if c /= c'
+              then let b1 = unsafeTake i ps
+                       b2 = unsafeDrop i ps
+                   in  return (b1, b2)
+              else go p (i+1)
+\end{code}
+%
+Via inference, \toolname verifies the safety of 
+the pointer accesses, and determines that the 
+sum of the lengths of the output pair of 
+@ByteString@s equals that of the input @ps@.
+@go@ terminates as @l-i@ is a well-founded 
+decreasing metric.
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End: 

commands.sty

+\usepackage[usenames,dvipsnames]{xcolor}
+
+ \def\mynote#1{{\sf $\clubsuit$ #1$\clubsuit$}}
+ \def\RJ#1{\textcolor{Red}{\sf RJ:$\clubsuit$ #1$\clubsuit$}}
+ \def\NV#1{\textcolor{Plum}{\sf NV:$\clubsuit$ #1$\clubsuit$}}
+ \def\ES#1{\textcolor{Blue}{\sf ES:$\clubsuit$ #1$\clubsuit$}}
+
+%%\def\RJ#1{}
+%%\def\NV#1{}
+%%\def\ES#1{}
+
+%%% \def\SPJ#1{\textcolor{Orange}{\sf SPJ:$\clubsuit$ #1$\clubsuit$}}
+
+\newcommand\todonum{\textcolor{Red}{XX}}
+
+\def\myex#1{\smallskip\noindent{\emphbf{Example: {#1}.}}}
+\newcommand\spara[1]{\smallskip\noindent\textbf{\emph{#1}}\xspace}
+\newcommand\mypara[1]{\spara{#1}}
+%\def\mypara#1{\smallskip\noindent\textbf{#1.}\ }
+
+
+
+\newcommand\etc{\textit{etc.}\xspace}
+\newcommand\eg{\textit{e.g.}\xspace}
+\newcommand\ie{\textit{i.e.}\xspace}
+\newcommand\ala{\textit{a la}\xspace}
+\newcommand\etal{\textit{et al.}\xspace}
+
+\def\emphbf#1{\textbf{\emph{#1}}}
+\def\spmid{\ \mid \ }
+
+\def\colon{\ensuremath{\text{:}}}
+
+\newcommand{\relDescription}[1]{\ensuremath{\textrm{\textbf{#1}}}}
+\newcommand{\judgementHead}[2]{\ensuremath{\relDescription{#1}\hfill\fbox{#2}}}
+\newcommand{\judgementHeadNameOnly}[1]{\ensuremath{\relDescription{#1}\hfill}}
+
+\newenvironment{sitemize}{\begin{list}
+   {$\bullet$}
+   {\setlength{\topsep}{0pt}
+    \setlength{\itemsep}{0pt}
+    \setlength{\leftmargin}{15pt}
+    }
+  }
+  {\end{list}}
+

conclusion.tex

+\chapter{Conclusion}
+In this report 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. 
+%
+To reason in such systems, we presented two alternatives:
+interactive theorem proving, where 
+the user should provide explicit proofs, and 
+contracts calculi, where 
+the assertions are verified at runtime.
+%
+Next we presented refinement type system 
+which restrict the refinement language, 
+so as to render type checking decidable.
+%thus both type checking and inference
+%is decidable.
+As an example, we presented Liquid Types, in which 
+the refinement language is restricted according to a finite set of qualifiers
+and allows not only decidable verification, but also automatic type inference.
+Then, we presented Abstract Refinement Types, which can be used
+in a refinement type system to enhance expressiveness without increasing complexity.
+Then,  we present \toolname
+that combines liquidTypes with abstraction over refinements
+to enhance expressiveness of LiquidTypes.
+\toolname is a quite expressive verification tool for Haskell programs 
+that can be used to check termination, 
+totality  and general functional correctness.
+Finally, we evaluate \toolname in real world Haskell libraries.
\ No newline at end of file

discussion.tex

+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End: 

examples.hs

+{-@ LIQUID "--short-names" @-}
+
+{-@ LIQUID "--no-termination" @-}
+
+module Ex (range, range', dup) where
+
+import Data.List (find)
+
+{-@ type Rng Lo Hi = {v:Int | (Lo <= v && v < Hi)} @-} 
+
+{-@ range :: lo:_ -> hi:{v:_ | lo <= v} -> [(Rng lo hi)] / [hi - lo] @-}
+range :: Int -> Int -> [Int]
+range lo hi 
+  | lo <= hi  = lo : range (lo + 1) (hi :: Int)
+  | otherwise = []
+
+{-@ range' :: lo:_ -> hi:_ -> [(Rng lo hi)] @-}
+range' lo hi = foldn lo hi (:) []  
+
+foldn :: Int -> Int -> (Int -> a -> a) -> a -> a
+foldn lo hi f = go lo hi 
+  where 
+    go i n acc  
+      | i < n     = go (i + 1) n (f i acc)
+      | otherwise = acc
+
+{-@ findInRange :: _ -> lo:_ -> hi:_ -> Maybe (Rng lo hi) @-}
+findInRange f lo hi = find f $ range lo hi
+
+{-@ measure evenL :: [a] -> Prop 
+    evenL ([])    = true
+    evenL (x:xs)  = not (evenL xs) 
+  @-}
+
+{-@ dup    :: [a] -> [a] @-}
+dup []     = []
+dup (x:xs) = x : x : dup xs 

haskellListings.tex

+\usepackage{listings}
+\usepackage[usenames,dvipsnames]{xcolor}
+
+\definecolor{gray_ulisses}{gray}{0.55}
+\definecolor{castanho_ulisses}{rgb}{0.71,0.33,0.14}
+\definecolor{preto_ulisses}{rgb}{0.41,0.20,0.04}
+\definecolor{green_ulises}{rgb}{0.2,0.75,0}
+
+\def\codesize{\normalsize}
+
+\lstdefinelanguage{HaskellUlisses} {
+	basicstyle=\ttfamily\codesize,
+	sensitive=true,
+	morecomment=[l][\color{gray_ulisses}\ttfamily\codesize]{--},
+	morecomment=[s][\color{gray_ulisses}\ttfamily\codesize]{\{-}{-\}},
+	morestring=[b]",
+	stringstyle=\color{red},
+	showstringspaces=false,
+	numberstyle=\codesize,
+	numberblanklines=true,
+	showspaces=false,
+	breaklines=true,
+	showtabs=false,
+	emph=
+	{[1]
+		FilePath,IOError,abs,acos,acosh,all,and,any,appendFile,approxRational,asTypeOf,asin,
+		asinh,atan,atan2,atanh,basicIORun,break,catch,ceiling,chr,compare,concat,concatMap,
+		const,cos,cosh,curry,cycle,decodeFloat,denominator,digitToInt,div,divMod,drop,
+		dropWhile,either,elem,encodeFloat,enumFrom,enumFromThen,enumFromThenTo,enumFromTo,
+		error,even,exp,exponent,fail,filter,flip,floatDigits,floatRadix,floatRange,floor,
+		fmap,foldl,foldl1,foldr,foldr1,fromDouble,fromEnum,fromInt,fromInteger,fromIntegral,
+		fromRational,fst,gcd,getChar,getContents,getLine,head,id,inRange,index,init,intToDigit,
+		interact,ioError,isAlpha,isAlphaNum,isAscii,isControl,isDenormalized,isDigit,isHexDigit,
+		isIEEE,isInfinite,isLower,isNaN,isNegativeZero,isOctDigit,isPrint,isSpace,isUpper,iterate,
+		last,lcm,length,lex,lexDigits,lexLitChar,lines,log,logBase,lookup,map,mapM,mapM_,max,
+		maxBound,maximum,maybe,min,minBound,minimum,mod,negate,not,notElem,null,numerator,odd,
+		or,ord,pi,primExitWith,print,product,properFraction,putChar,putStr,putStrLn,quot,
+		quotRem,range,rangeSize,read,readDec,readFile,readFloat,readHex,readIO,readInt,readList,readLitChar,
+		readLn,readOct,readParen,readSigned,reads,readsPrec,realToFrac,recip,rem,repeat,replicate,return,
+		reverse,round,scaleFloat,scanl,scanl1,scanr,scanr1,seq,sequence,sequence_,show,showChar,showInt,
+		showList,showLitChar,showParen,showSigned,showString,shows,showsPrec,significand,signum,sin,
+		sinh,snd,span,splitAt,sqrt,subtract,succ,sum,tail,take,takeWhile,tan,tanh,threadToIOResult,toEnum,
+		toInt,toInteger,toLower,toRational,toUpper,truncate,uncurry,undefined,unlines,until,unwords,unzip,
+		unzip3,userError,words,writeFile,zip,zip3,zipWith,zipWith3,listArray,doParse,empty,for,initTo,
+        maxEvens,empty,create,get,set,initialize,idVec,fastFib,fibMemo,
+        insert,union,fromList,initUpto,trim,quickSort,insertSort,append,upperCase,
+        pred, sig, two_gt0, safeDiv, terminates, loop, go, incr, plusminus, plus, minus, zgtz
+	},
+	emphstyle={[1]\color{blue}},
+	emph=
+	{[2]
+		Bool,Char,Double,Either,Float,IO,Integer,Int,Maybe,Ordering,Rational,Ratio,ReadS,ShowS,String,
+		Word8,InPacket,Tree,Vec,List,C,N,NullTerm,IncrList,DecrList,UniqList,BST,MinHeap,MaxHeap
+	},
+	emphstyle={[2]\color{castanho_ulisses}},
+	emph=
+	{[3]
+		case,class,data,deriving,do,else,if,import,in,infixl,infixr,instance,let,
+		module,measure,of,primitive,then,refinement,type,where, exists
+	},
+	emphstyle={[3]\color{preto_ulisses}\textbf},
+	emph=
+	{[4]
+		quot,rem,div,mod,elem,notElem,seq
+	},
+	emphstyle={[4]\color{castanho_ulisses}\textbf},
+	emph=
+	{[5]
+		EQ,False,GT,Just,LT,Left,Nothing,Right,True,Show,Eq,Ord,Num,
+		S
+	},
+	emphstyle={[5]\color{preto_ulisses}\textbf},
+	emph=
+	{[7]
+		Type, Prop
+	},
+	emphstyle={[7]\color{Blue}\textbf},
+	emph=
+	{[8]
+		exist, eq_refl, nat
+	},	
+	emphstyle={[8]\color{castanho_ulisses}}
+}
+
+%%%ORIG
+%%%\lstnewenvironment{code}
+%%%{\textbf{Haskell Code} \hspace{1cm} \hrulefill \lstset{language=HaskellUlisses}}
+%%%{\hrule\smallskip}
+
+%V1
+%\lstnewenvironment{code}
+%{\smallskip \lstset{language=HaskellUlisses}}
+%{\smallskip}
+
+
+\lstdefinelanguage{CoqUlisses} {
+	basicstyle=\ttfamily\codesize,
+	sensitive=true,
+	morecomment=[l][\color{gray_ulisses}\ttfamily\codesize]{--},
+	morecomment=[s][\color{gray_ulisses}\ttfamily\codesize]{\{-}{-\}},
+	morestring=[b]",
+	stringstyle=\color{red},
+	showstringspaces=false,
+	numberstyle=\codesize,
+	numberblanklines=true,
+	showspaces=false,
+	breaklines=true,
+	showtabs=false,
+	emph=
+	{[1]
+		FilePath,IOError,abs,acos,acosh,all,and,any,appendFile,approxRational,asTypeOf,asin,
+		asinh,atan,atan2,atanh,basicIORun,break,catch,ceiling,chr,compare,concat,concatMap,
+		const,cos,cosh,curry,cycle,decodeFloat,denominator,digitToInt,div,divMod,drop,
+		dropWhile,either,elem,encodeFloat,enumFrom,enumFromThen,enumFromThenTo,enumFromTo,
+		error,even,exp,exponent,fail,filter,flip,floatDigits,floatRadix,floatRange,floor,
+		fmap,foldl,foldl1,foldr,foldr1,fromDouble,fromEnum,fromInt,fromInteger,fromIntegral,
+		fromRational,fst,gcd,getChar,getContents,getLine,head,id,inRange,index,init,intToDigit,
+		interact,ioError,isAlpha,isAlphaNum,isAscii,isControl,isDenormalized,isDigit,isHexDigit,
+		isIEEE,isInfinite,isLower,isNaN,isNegativeZero,isOctDigit,isPrint,isSpace,isUpper,iterate,
+		last,lcm,length,lex,lexDigits,lexLitChar,lines,log,logBase,lookup,map,mapM,mapM_,max,
+		maxBound,maximum,maybe,min,minBound,minimum,mod,negate,not,notElem,null,numerator,odd,
+		or,ord,pi,primExitWith,print,product,properFraction,putChar,putStr,putStrLn,quot,
+		quotRem,range,rangeSize,read,readDec,readFile,readFloat,readHex,readIO,readInt,readList,readLitChar,
+		readLn,readOct,readParen,readSigned,reads,readsPrec,realToFrac,recip,rem,repeat,replicate,
+		reverse,round,scaleFloat,scanl,scanl1,scanr,scanr1,seq,sequence,sequence_,show,showChar,showInt,
+		showList,showLitChar,showParen,showSigned,showString,shows,showsPrec,significand,signum,sin,
+		sinh,snd,span,splitAt,sqrt,subtract,succ,sum,tail,take,takeWhile,tan,tanh,threadToIOResult,toEnum,
+		toInt,toInteger,toLower,toRational,toUpper,truncate,uncurry,undefined,unlines,until,unwords,unzip,
+		unzip3,userError,words,writeFile,zip,zip3,zipWith,zipWith3,listArray,doParse,empty,for,initTo,
+        maxEvens,empty,create,get,set,initialize,idVec,fastFib,fibMemo,
+        insert,union,fromList,initUpto,trim,quickSort,insertSort,append,upperCase, 
+        pred, sig, two_gt0, zgtz
+	},
+	emphstyle={[1]\color{blue}},
+	emph=
+	{[2]
+		Bool,Char,Double,Either,Float,IO,Integer,Int,Maybe,Ordering,Rational,Ratio,ReadS,ShowS,String,
+		Word8,InPacket,Tree,Vec,NullTerm,IncrList,DecrList,UniqList,BST,MinHeap,MaxHeap,
+		exist, eq_refl, nat
+	},
+	emphstyle={[2]\color{castanho_ulisses}},
+	emph=
+	{[3]
+		case,class,data,deriving,do,else,if,import,in,infixl,infixr,instance,let,
+		module,measure,of,primitive,then,refinement,type,where,return,match, with, end,
+		forall, fun
+	},
+	emphstyle={[3]\color{Blue}},
+	emph=
+	{[4]
+		quot,rem,div,mod,elem,notElem,seq
+	},
+	emphstyle={[4]\color{castanho_ulisses}\textbf},
+	emph=
+	{[5]
+		EQ,False,GT,Just,LT,Left,Nothing,Right,True,Show,Eq,Ord,Num,S
+	},
+	emphstyle={[5]\color{preto_ulisses}\textbf},
+    emph=
+    {[6]	
+		Definition, Inductive, Notation
+	},
+	emphstyle={[6]\color{BurntOrange}\textbf},
+	emph=
+	{[7]
+		Type, Prop
+	},
+	emphstyle={[7]\color{Blue}\textbf},
+}
+
+\lstnewenvironment{codeCoq}
+{\lstset{language=CoqUlisses}}
+{}
+
+\lstnewenvironment{code}
+{\lstset{language=HaskellUlisses}}
+{}
+
+\lstMakeShortInline[language=HaskellUlisses]@

hscolour.tex

+\begin{itemize}
+\item Reading the input.
+@HsColour.hs@ reads the input arguments and checks their well-formedness
+using the when statement
+%
+\begin{code}
+when (length outFile > 1) \$ errorOut "Can only have one output file"
+\end{code}
+%
+Currently \toolname can not take advantage of such specifications, 
+thus explicit @assume@ is used.
+
+\item Lists with structure:
+@ACSS.splitSrcAndAnnos@ handles a list of Strings and makes the following assumption.
+when the specific @breakS@ appears then the name and annotations follow (ie., at least two elements).
+So if a list @ls@ starts with @breakS@ then it uses an refutable pattern  @(_:mname:annots) = ls@
+to match the list.
+This invariant about the inputs list cannot be proven statically.
+Worse, \toolname has no way to express such invariant, 
+as refinement of list elements \textit{relies} on polymorphism: 
+\toolname naturally describes invariants that recursively hold for every list element and 
+reaches it edge when reasoning about non-recursive properties.
+
+\item The instance @Enum@ of @Highlight@ does not define the @toEnum@ method, 
+which as discussed reduces to a @noMethodBinding@ error that makes verification unsafe.
+
+\item trimContext initially checks whether there exists an element that satisfies @p@ in the list @xs@.
+If it is it creates @ys = dropWhile (not p) xs@, and then calls the tail of @ys@.
+By the check we know that @ys@ has at least one element, the one that satisfies @p@, 
+a property that is not trivially expressed via refinement types.
+
+
+\item filter data constructors: @foo (filter (`elem` [A, B, C])@ and then partially define 
+@foo@ on only the data constructors @A@, @B@, and @C@.
+\end{itemize}

intro.tex

+\section{Intro --- Verification with Dependent Types}
+
+Specify and enforce rich data invariants.
+\begin{itemize}
+\item Higher-order logics, ie, Coq, F$\star$, Agda, 
+expressive, but undecidable --- interactive proofs
+\item Annotate program --- lower annotation burden \cite{OuTMW04} 
+Static $\Rightarrow $ restrict expressiveness or dynamic checking
+\end{itemize}

liquidHaskell.sty

+\usepackage{color}
+\usepackage{textcomp}
+\newcommand\highlight[2]{{\setlength\fboxsep{1pt}\colorbox{#1}{#2}}}
+
+
+%\def\NV{\highlight{colorNV}}
+\definecolor{colorNV}{rgb}{1,0.8,1}
+
+\providecommand{\dbrkts}[1]{[\![#1]\!]}
+
+\newenvironment{grammar}{\csname align*\endcsname}{\csname endalign*\endcsname}
+\newcommand\grammardef[2]{\ensuremath{#1\ \text{::}&\text{=} && \text{\textit{#2}}}\\}
+\newcommand\grammardefnoalt[3]{\ensuremath{#1\ \text{::}&\text{=} #2 && \text{\textit{#3}}}\\}
+\newcommand\grammardefbare[2]{\ensuremath{#1\ \ & && \text{\textit{#2}}}\\}
+\newcommand\grammaralt[2]{\ensuremath{&\mid #1 && \text{#2}}\\}
+
+
+\newcommand\phide[1]{}
+\newcommand\lhide[1]{}
+\newcommand\hide[1]{}
+
+\newcommand\rulename[1]{\textsc{#1}\xspace}
+
+\newcommand\hastype[3]{\ensuremath{#1 \vdash #2 : #3}}
+\newcommand\eval[2]{\ensuremath{#1 \hookrightarrow #2 }}
+
+
+%predicate type
+\newcommand\predty{\ensuremath{t}}
+
+
+%basic
+\newcommand\vref{\ensuremath{v}}
+\newcommand\tyDef[1]{\ensuremath{\mathbb{#1}}}
+\newcommand\tyDefArg[2]{\ensuremath{\tyDef{#1}\left(\tyDef{#2}\right)}}
+\newcommand\nhaskell[1]{\mathsf{#1}}
+
+
+%rule names
+\newcommand\tfunction{\rulename{T-Fun}}
+\newcommand\tapp{\rulename{T-App}}
+\newcommand\tsub{\rulename{T-Sub}}
+\newcommand\tconst{\rulename{T-Const}}
+\newcommand\tinst{\rulename{T-Inst}}
+\newcommand\tgen{\rulename{T-Gen}}
+\newcommand\tpinst{\rulename{T-Inst}}
+\newcommand\tpgen{\rulename{T-Gen}}
+\newcommand\tcase{\rulename{T-Case}}
+\newcommand\tbase{\rulename{T-Var-Base}}
+\newcommand\tvariable{\rulename{T-Var}}
+
+
+\newcommand\wsEmp{\rulename{WS-Empty}}
+\newcommand\wsExt{\rulename{WS-Ext}}
+\newcommand\wsGxt{\rulename{WS-Gxt}}
+
+\newcommand\wstEmp{\rulename{WTS-Empty}}
+\newcommand\wstExt{\rulename{WTS-Ext}}
+\newcommand\wstGxt{\rulename{WTS-Gxt}}
+
+\newcommand\wtTrue{\rulename{WF-True}}
+\newcommand\wtRVApp{\rulename{WF-RApp}}
+\newcommand\wtVar{\rulename{WF-Var}}
+\newcommand\wtBase{\rulename{WF-Base}}
+\newcommand\wtFun{\rulename{WF-Fun}}
+\newcommand\wtApp{\rulename{WF-App}}
+\newcommand\wtPred{\rulename{WF-Abs}}
+\newcommand\wtPoly{\rulename{WF-Abs-$\alpha$}}
+
+\newcommand\tdsubBase{$\subt$\rulename{-Dec-Base}}
+\newcommand\tsubBase {$\subt$\rulename{-Base}}
+\newcommand\tsubFun  {$\subt$\rulename{-Fun}}
+\newcommand\tsubVar  {$\subt$\rulename{-Var}}
+\newcommand\tsubApp  {$\subt$\rulename{-App}}
+\newcommand\tsubClass{$\subt$\rulename{-Class}}
+\newcommand\tsubPred {$\subt$\rulename{-Abs}}
+\newcommand\tsubPoly {$\subt$\rulename{-Poly}}
+
+
+\def\subt{\prec}
+
+
+\newcommand\hasType[4]{\ensuremath{#1 \vdash_{#2} #3 : #4 }}
+\newcommand\hasTypeP[4]{\ensuremath{#1 \vdash #2 : #3 \mid #4 }}
+\newcommand\penv{\ensuremath{\Gamma}}
+\newcommand\isSubType[3]{\ensuremath{#1 \vdash \subtype{#2}{#3}}}
+\newcommand\subtype[2]{\ensuremath{#1 \preceq #2}}
+\newcommand\isWellFormed[2]{\ensuremath{#1 \vdash #2 }}
+\newcommand\isWellFormedP[3]{\ensuremath{#1, #2 \vdash #3 }}
+\newcommand\meet[2]{\ensuremath{\text{meet} \left( {#1}, {#2} \right)}}
+\newcommand\strengthen[2]{\ensuremath{\text{strengthen} \left( {#1}, {#2} \right)}}
+\newcommand\shape[1]{\ensuremath{\text{shape} \left( {#1} \right)}}
+\newcommand\shapep[1]{\ensuremath{\text{shapep} \left( {#1} \right)}}
+
+\newcommand\isSub[3]{\ensuremath{{#1}\vdash {#2}<:{#3}}}
+%\newcommand\eval[2]{\ensuremath{{#1}\looparrowright {#2}}}
+%\newcommand\eval[2]{\ensuremath{{#1}\hookrightarrow {#2}}}
+
+\newcommand\hastypeEmp[2]{\hastype{\emptyset}{#1}{#2}}
+\newcommand\isSubEmp[2]{\isSub{\emptyset}{#1}{#2}}
+
+
+\newcommand\sch[1]{\ensuremath{\texttt{Schema}\left(#1\right)}}
+\newcommand\fv[1]{\ensuremath{\texttt{FreeVars}\left(#1\right)}}
+
+
+
+%expressions
+\newcommand\etabs[2]{\ensuremath{\Lambda #1 . #2}}
+\newcommand\epabs[3]{\ensuremath{\Lambda {#1:#2} . #3}}
+
+\newcommand\efunt[3]{\ensuremath{\lambda {#1:#2}. #3}}
+\newcommand\efunbar[2]{\ensuremath{\lambda \overline{#1} . #2}}
+%\newcommand\efun[2]{\ensuremath{\lambda #1 . #2}}
+\newcommand\eapp[2]{\ensuremath{{#1} \ {#2}}}
+\newcommand\etapp[2]{\ensuremath{{#1} \left[ {#2}\right]}}
+\newcommand\epapp[2]{\ensuremath{{#1} \left[ #2\right]}}
+
+
+\newcommand\elam[2]{\efun{#1}{#2}}
+\newcommand\eplam[2]{\ensuremath{\epabs{#1}{#2}}}
+\newcommand\etlam[2]{\ensuremath{\etabs{#1}{#2}}}
+
+\newcommand\elet[3]{\ensuremath{\nhaskell{let} \ #1 = #2 \ \nhaskell{in} \ #3}}
+\newcommand\eletrec[3]{\ensuremath{\nhaskell{let rec} \ #1 = #2 \ \nhaskell{in} \ #3}}
+\newcommand\ecase[4]{\ensuremath{\nhaskell{case} \ (#1 = #2) \ \nhaskell{of} \ \mid_i  #3 \ \rightarrow \ #4}}
+
+%translation
+
+\newcommand\tx[1]{\ensuremath{\langle\!| #1 |\!\rangle}}
+\newcommand\txinv[1]{\ensuremath{\langle| #1 |\rangle^{-1}}}
+%%\newcommand\tx[1]{\ensuremath{\text{tx}(#1)}}
+%%\newcommand\txinv[1]{\ensuremath{\text{tx}^{-1}(#1)}}
+\newcommand\isWellFormedH[2]{\ensuremath{\tx{#1} \vdash_H \tx{#2}}}
+\newcommand\isSubTypeH[3]{\ensuremath{\tx{#1} \vdash_H {\tx{#2}} <: {\tx{#3}}}}
+\newcommand\hastypeH[3]{\ensuremath{#1 \vdash_H #2 : #3}}
+
+
+
+
+%types
+\newcommand\conlan{\ensuremath{\mathrm{F_H}}\xspace}
+\newcommand\corelan{$\lambda_{P}$\xspace}
+\newcommand\corelanm{$\lambda_{LP}$'\xspace}
+
+\newcommand{\reft}{\ensuremath{e}\xspace}
+\newcommand{\areft}{\ensuremath{p}\xspace}
+\newcommand\rvapp[2]{\ensuremath{{#1 \ \overline{#2}}}} 
+\newcommand\tref[2]{\ensuremath{\left\lbrace \vref : #1\mid #2\right\rbrace}}
+\newcommand{\tpp}[2]{{#1 \langle #2 \rangle}}
+\newcommand\tpref[3]{\tref{\tpp{#1}{#2}}{#3}}
+
+\newcommand\tbint{\ensuremath{\texttt{int}}\xspace}
+\newcommand\tbbool{\ensuremath{\texttt{bool}}\xspace}
+\newcommand\tc[1]{\ensuremath{tc\left(#1\right)}}
+\newcommand\tfun[3]{\ensuremath{{#1:#2} \rightarrow #3}}
+\newcommand\tcfun[2]{\ensuremath{{#1 \rightarrow #2}}}
+\newcommand\ptype[1]{\tcfun{#1}{\tbbool}}
+\newcommand\rpinst[3]{\ensuremath{{#1}[{#2} \vartriangleright {#3}]}}
+\newcommand\rpapply[5]{\ensuremath{\mathsf{Apply}(#1,#2,#3,#4,#5)}}
+
+
+
+\newcommand\trfun[4]{\ensuremath{\tref{\tfun{#1}{#2}{#3}}{#4}}}
+\newcommand\trfuntop[3]{\ensuremath{#1 : #2 \rightarrow #3}}
+\newcommand\tpabs[3]{\ensuremath{\forall #1 : #2 . #3}}
+\newcommand\ttabs[2]{\ensuremath{\forall #1 . #2}}
+
+
+\newcommand\tbool{\tbbool}
+\newcommand\tvar[2]{\tref{#1}{#2}}
+\newcommand\tcon[4]{\ensuremath{\tref{\nhaskell{#1} \ #3 \ #4}{#2}}}
+\newcommand\tclass[2]{\ensuremath{\nhaskell{#1} \ #2}}
+\newcommand\tforallPr[2]{\ensuremath{\forall #1 . #2}}
+\newcommand\tforallTy[2]{\ttabs{#1}{#2}}
+
+
+\newcommand\pdVar[3]{\ensuremath{#1}} %it seems that the pred var is just a var...
+%\newcommand\pdVar[3]{\ensuremath{#1 : #2 \left\langle #3 \right\rangle }}
+
+\newcommand\unifyTypes[3]{\ensuremath{ \left\langle {#1} , {#2} \right\rangle \models {#3}}}
+\newcommand\refa[3]{\ensuremath{ \left\lbrace #1 : #2 \mid #3 \right\rbrace }}
+\newcommand\sub[2]{\ensuremath{ \left[ #1 \mapsto #2 \right] }}
+\newcommand\subP[2]{\ensuremath{\left[#1\mapsto_\star #2\right]}}
+\newcommand\freshP[1]{\ensuremath{\text{fresh}\ \left( #1\right)}}
+\newcommand\freshT[1]{\ensuremath{\text{fresh}\ \left( #1\right)}}
+\newcommand\subT[2]{\ensuremath{\sub{#1}{#2}}}
+
+
+\newcommand\pdTy{\ensuremath{{T_P}}}
+\newcommand\lTy{\ensuremath{\hat{T}}}
+\newcommand\dTy{\ensuremath{T}}
+
+\newcommand\appTy[2]{\ensuremath{\parAny{#1} \left( #2 \right)  }}
+\newcommand\parTy[2]{\ensuremath{\parAny{#1} \left( \parAny{#2} \right)  }}
+\newcommand\parAny[1]{\ensuremath{\mathbb{#1}}}
+\newcommand\listOf[1]{\ensuremath{\left\langle #1 \right\rangle}}
+
+
+\newcommand\tyConPs[1]{\ensuremath{\text{predicates} \left( #1 \right)}}
+\newcommand\valid[2]{\ensuremath{#1 \Rightarrow #2}}
+\newcommand\inter[1]{\ensuremath{\dbrkts{#1}}}

main.tex

+%documentclass{llncs}
+\documentclass[runningheads,a4paper]{article}
+%%% \usepackage[top=1.5cm,bottom=1.5cm,left=2.3cm,right=2cm]{geometry}
+
+\pagestyle{plain}
+\usepackage{times}
+%\usepackage[nocompress]{cite} % AR: comment this out if you wish hyperrefs 
+
+\usepackage{amsmath,amssymb, latexsym}
+
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+
+\usepackage{liquidHaskell}
+\usepackage[inference]{semantic}
+
+\newcommand\etal{et al.\xspace}
+
+%\usepackage{subfigure}
+%\usepackage{graphicx}
+%\usepackage[usenames,dvipsnames]{color}
+\usepackage{enumerate}
+\def\url{}
+\usepackage{xspace}
+\usepackage{epsfig}
+\usepackage{mathpartir}
+\usepackage{booktabs}
+
+%\usepackage{extarrows}
+%\usepackage{pgf,tikz}
+%\usetikzlibrary{arrows,automata}
+
+
+\newcommand{\isTechReport}{false} % true or false
+\newcommand{\includeProof}[1]{
+  \ifthenelse{\equal{\isTechReport}{true}}{
+    #1
+  }{
+  }
+}
+
+\newcommand{\at}{\makeatletter @\makeatother}
+
+%%%%%\usepackage{fancyvrb}
+%%%%%\DefineVerbatimEnvironment{code}{Verbatim}{fontsize=\small}
+%%%%%\DefineVerbatimEnvironment{example}{Verbatim}{fontsize=\small}
+%%%%%\newcommand{\ignore}[1]{}
+
+% command to end a proof or definition:
+%\def\qed{\rule{0.4em}{1.4ex}}
+\def\qed{\hfill$\Box$}
+
+% space at the beginning of an environment:
+\def\@envspa{\hspace{0.3em}}
+\def\@sa{\hspace{-0.2em}}
+\def\@sb{\hspace{0.5em}}
+\def\@sc{\hspace{-0.1em}}
+
+\def\sk{\smallskip}		% space before and after theorems
+
+\input{commands}
+\input{haskellListings}
+
+
+
+\sloppy
+\newcommand\mytitle{LiquidHaskell: Liquid Types for Haskell} 
+
+\newcommand\myauthor{Niki Vazou}
+\newcommand\institution{University of California, San Diego}
+\newcommand\myemail{nvazou\at cs.ucsd.edu}
+
+\newcommand{\mymaketitle}{
+  \begin{center}
+  	{\LARGE\bf \mytitle \\ \vspace{1cm}}%
+    {\Large \myauthor \\}%
+ 	{\large \myemail \\}%
+  	{\large \institution \\}%
+  \end{center}
+  \par} 
+
+
+\begin{document}
+\mymaketitle
+\begin{abstract}
+\input{abstract}
+\end{abstract}
+
+
+\input{dependent}
+\input{undecidable}
+\input{liquid}
+\input{abstract_refinements}
+\input{tool}
+\input{totality}
+\input{termination}
+\input{structures}
+\input{evaluation}
+\input{conclusion}
+
+{
+\bibliographystyle{plain}
+\bibliography{sw}
+}
+
+\end{document}
\ No newline at end of file

main.tex.old

+\documentclass{sigplanconf}
+%%% \usepackage[top=1.5cm,bottom=1.5cm,left=2.3cm,right=2cm]{geometry}
+
+\pagestyle{plain}
+\usepackage{times}
+%\usepackage[nocompress]{cite} % AR: comment this out if you wish hyperrefs 
+\usepackage{hyperref}
+
+\usepackage{amsmath,amssymb, latexsym}
+
+\usepackage{amsmath}
+\usepackage{amsthm}
+
+\usepackage{comment}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{mathtools}
+\usepackage{commands}
+\usepackage{liquidHaskell}
+\usepackage[inference]{semantic}
+\usepackage{enumerate}
+%\def\url{}
+\usepackage{xspace}
+\usepackage{epsfig}
+\usepackage{booktabs}
+\usepackage{listings}
+\usepackage{comment}
+\usepackage{ifthen}
+\usepackage{flushend}
+\newcommand\includeBytestring[1]{}
+
+% space at the beginning of an environment:
+\def\@envspa{\hspace{0.3em}}
+\def\@sa{\hspace{-0.2em}}
+\def\@sb{\hspace{0.5em}}
+\def\@sc{\hspace{-0.1em}}
+
+\def\sk{\smallskip}		% space before and after theorems
+
+\input{haskellListings}
+
+\begin{document}
+
+\conferenceinfo{Haskell~'14}{September 6, 2014, Gothenburg, Sweden}
+\copyrightyear{2014}
+\copyrightdata{978-1-4503-3041-1/14/09}
+\doi{2633357.2633366} 
+
+\title{LiquidHaskell: Experience with Refinement Types in the Real World 
+        \thanks{This work was supported by NSF grants 
+          CNS-0964702, CNS-1223850, CCF-1218344, CCF-1018672,
+          and a generous gift from Microsoft Research.
+        }}
+%\title{LiquidHaskell: Liquid Types for Real Haskell Programs} 
+
+\authorinfo{Niki Vazou \and Eric L. Seidel \and Ranjit Jhala}{UC San Diego}{}
+
+\maketitle
+%% CLEAR ENOUH WITH CITATION? \NV{(R2)
+%% CLEAR ENOUH WITH CITATION? make clear what the relationship of this work is to the authors'
+%% CLEAR ENOUH WITH CITATION? related paper appearing in ICFP '14, and what the novelty of this
+%% CLEAR ENOUH WITH CITATION? paper is in comparison to it.  For instance, the evaluation section of
+%% CLEAR ENOUH WITH CITATION? }
+
+%% FIXED \NV{(R3)
+%% FIXED You mention that totality checks are w.r.t. Core.  
+%% FIXED Are errors then also w.r.t. Core?}
+
+%% FIXED \NV{(R2)
+%% FIXED  Although the abstract mentions "a combination of refinement types
+%% FIXED  and SMT solvers", the paper never mentions SMT solvers again
+%% FIXED  except for a brief mention of Z3 in passing on page 9 and in the
+%% FIXED  related work on page 11.
+%% FIXED }
+
+%% LIMITATIONS \NV{(R3) Lessons learned:debugging the (not-so-friendly) SMT output?}
+
+%% LIMITATIONS \NV{(R3)
+%% LIMITATIONS Is there anything you couldn't verify (e.g., libraries that use 
+%% LIMITATIONS non-linear arithmetic or alternating quantifiers in the 
+%% LIMITATIONS specifications?  If not, why? State, average
+%% LIMITATIONS }
+
+%% UNCLEAR \NV{(R4)
+%% UNCLEAR The document is not intended to describe the structure of LH, 
+%% UNCLEAR however many develops with correctness concerns continue to 
+%% UNCLEAR pick and choose their underlying prover carefully.  
+%% UNCLEAR Whether or not the SMT solver is interchangeable 
+%% UNCLEAR interests audiences likely to put LH into practice.
+%% UNCLEAR }
+\input{abstract}
+\input{intro}
+\input{tool}
+\input{totality}
+\input{termination}
+\input{memory-safety}
+\input{structures}
+
+%% \input{xmonad}
+%% \input{redblack}
+
+\input{evaluation}
+%\input{discussion}
+\input{related}
+\input{conclusion}
+\subsection*{Acknowledgements}
+We thank Dimitrios Vytiniotis and Simon Peyton-Jones for inspiring 
+our work on checking totality. 
+Also, we thank Colin S. Gordon and users of \toolname for their feedback
+and bug reports.
+
+{
+\bibliographystyle{plain}
+\bibliography{sw}
+}
+
+
+\end{document}

memory-safety.tex

+\section{Memory Safety}\label{sec:memory-safety}
+
+The terms ``Haskell'' and ``pointer arithmetic'' rarely occur in the same
+sentence, yet many Haskell programs are constantly manipulating pointers under
+the hood by way of using the \bytestring and \libtext libraries. These libraries
+sacrifice safety for (much needed) speed and are therefore natural candidates for
+verification through \toolname.
+
+\subsection{Bytestring}\label{sec:bytestring}
+\input{bytestring}
+
+\subsection{Text}\label{sec:text}
+\input{text}
+
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End: 

redblack.tex

+
+  
+

related.tex

+\section{Related Work}\label{sec:related}
+
+Next, we situate \toolname with 
+existing Haskell verifiers.
+
+\spara{Dependent Types} are the basis of many verifiers, 
+or more generally, proof assistants.
+%
+Verification of haskell code is possible with
+``full'' dependently typed systems like Coq~\cite{coq-book}, 
+Agda~\cite{norell07}, Idris~\cite{Brady13}, Omega~\cite{Sheard06}, and
+ {$\lambda_\rightarrow$}~\cite{LohMS10}.
+ %
+ While these systems are highly expressive,
+their expressiveness comes at the cost of making logical validity checking undecidable
+thus rendering verification cumbersome.	
+ %
+ Haskell itself can be considered a dependently-typed language,
+ as type level computation is allowed via 
+ Type Families~\cite{McBride02},
+ Singleton Types\cite{Weirich12}, 
+ Generalized Algebraic  Datatypes (GADTs)~\cite{JonesVWW06, SchrijversJSV09}, 
+ % more GADS ~\cite{Cheney02, GRDC03},
+ and type-level functions~\cite{ChakravartyKJ05}.
+ %
+Again, 
+verification in haskell itself turns out to be quite painful~\cite{LindleyM13}.
+
+\spara{Refinement Types} are a form of dependent types where 
+invariants are encoded via a combination of types and predicates
+from a restricted \emph{SMT-decidable} 
+logic~\cite{Rushby98,pfenningxi98,Dunfield07,GordonTOPLAS2011}. 
+%
+\toolname uses Liquid Types~\cite{LiquidPLDI09} 
+that restrict the invariants even more
+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} 
+with sophisticated measure definitions 
+allows specification and verification of a wide variety 
+of program properties.
+
+\spara{Static Contract Checkers} 
+like ESCJava~\cite{ESCJava} are a classical way of verifying 
+correctness through assertions and pre- and post-conditions. 
+%
+%
+%% One can view Refinement Types as a type-based 
+%% generalization of this approach. 
+%
+%% Classical contract checkers check ``partial''
+%% (as opposed to ``total'') correctness (\ie safety) 
+%% for \emph{eager}, typically first-order, languages
+%% and need not worry about termination.
+%% %
+%% We have shown that in the lazy setting, even 
+%% ``partial'' correctness requires proving ``total''
+%% correctness!
+%
+\cite{XuPOPL09} describes a static contract checker for 
+Haskell that uses symbolic execution to unroll procedures
+upto some fixed depth, yielding weaker ``bounded'' soundness
+guarantees.
+% 
+%% The (checker's) termination requires that recursive 
+%% procedures only be unrolled up to some fixed depth.
+%% While this approach removes inconsistencies, it yields 
+%% weaker, ``bounded'' soundness guarantees.
+%
+Similarly, Zeno~\cite{ZENO} is an automatic Haskell 
+prover that combines unrolling with heuristics for rewriting
+and proof-search. 
+%%Based on rewriting, it is sound but 
+%%``Zeno might loop forever'' when faced with 
+%%non-termination.
+%
+Finally, the Halo~\cite{halo} contract checker encodes 
+Haskell programs into first-order logic by directly 
+modeling the code's denotational semantics,
+again, requiring heuristics for instantiating axioms 
+describing functions' behavior.
+%
+%%Unlike any of the above, our type-based approach does 
+%%not rely on heuristics for unrolling recursive procedures, 
+%%or instantiating axioms. 
+%%%
+%%Instead we are based on decidable SMT validity 
+%%checking and abstract interpretation~\cite{LiquidPLDI08} 
+%%which makes the tool predictable and the overall workflow
+%%scale to the verification of large, real-world
+%%code bases.
+%%
+%%
+%%\spara{Tracking Divergent Computations}
+%%The notion of type stratification to track potentially 
+%%diverging computations dates to at least~\citep{ConstableS87} 
+%%which uses %$\bar{\typ}$ 
+%%to encode diverging terms, and types 
+%%%$\efix{}$ as $(\bar{\typ}\rightarrow\bar{\typ}) \rightarrow \bar{\typ}$).
+%%%
+%%More recently, \cite{Capretta05} tracks diverging 
+%%computations within a \emph{partiality monad}.
+%%%
+%%Unlike the above, we use refinements to 
+%%obtain terminating fixpoints %(\etfix{}), 
+%%which let us prove 
+%%the vast majority (of sub-expressions) in real world libraries 
+%%as non-diverging, avoiding the restructuring that would
+%%be required by the partiality monad.
+%%
+
+\spara{Totality Checking}
+is feasible by GHC itself, via an option flag that warns of any incomplete patterns.
+%
+Regrettably, GHC's warnings are local, \ie
+GHC will raise a warning for @head@'s partial definition, 
+but not for its caller, as the programmer would desire.
+%%(2)~ and preservative:
+%%a warning will be raised for any incomplete pattern
+%%without an attempt to reason if it is reachable or not.
+%
+Catch~\cite{catch}, 
+a fully automated tool that tracks incomplete patterns,
+addresses the above issue
+%
+by computing functions' pre- and post-conditions.
+Moreover, catch statically analyses the code 
+to track reachable incomplete patterns.
+%
+\toolname allows more precise analysis than catch, 
+thus, by assigning the appropriate
+types to $\star$Error functions (\S~\ref{sec:totality}) 
+it tracks reachable incomplete patters 
+%we get catch analysis
+as a side-effect of verification.
+
+\spara{Termination Analysis}
+is crucial for \toolname's soundness~\cite{LiquidICFP14} 
+and is implemented in a technique inspired by~\cite{XiTerminationLICS01}, 
+%
+Various other authors have proposed techniques to verify termination of
+recursive functions, either using the ``size-change
+principle''~\cite{JonesB04,Sereni05}, or by annotating types with size indices
+and verifying that the arguments of recursive calls have smaller
+indices~\cite{HughesParetoSabry96,BartheTermination}.
+%
+To our knowledge, none of the above analyses have been empirically
+evaluated on large and complex real-world libraries.
+
+AProVE~\cite{Giesl11} implements a powerful, fully-automatic
+termination analysis for Haskell based on term-rewriting.
+%
+Compared to AProVE,
+encoding the termination proof via 
+refinements provides advantages that are crucial in 
+large, real-world code bases. 
+Specifically, refinements
+let us
+%
+(1) prove termination over a subset 
+    (not all) of inputs; many functions (\eg @fac@) 
+    terminate only on @Nat@ inputs and not all @Int@s,
+%
+(2) encode pre-conditions, 
+    post-conditions, and auxiliary invariants that 
+    are essential for proving termination, (\eg @qsort@),
+%
+(3) easily specify non-standard 
+    decreasing metrics and prove termination, (\eg @range@).
+%
+In each case, the code could be (significantly) 
+\emph{rewritten} to be amenable to AProVE but this defeats
+the purpose of an automatic checker.
+%
+
+
+% Could use APROVE, but didn't
+% 1. refinements let us reason about /partial functions/
+% 2. refinements let us reason about /auxiliary invariants/
+% 3. refinements let us specify witness expressions for termination
+
+% Given the existence of such standalone termination provers, one might
+% ask why we chose to prove termination ourselves. While certainly
+%% We could use one such existing termination analysis; however, we found that
+%% encoding the termination proof via refinements provided a synergy that
+%% would have been impossible with an external oracle. 
+%% %
+%% Specifically, we
+%% found that 
+%% (1) refinements let us prove termination of \emph{partial functions},
+%% (2) refinements let us reason about \emph{auxiliary invariants}, and 
+%% (3) refinements let us express termination metrics that require 
+%%     a \emph{witness} without editing the actual code.
+
+% Given our the structure of our proof, with the Termination Oracle
+% Hypothesis, one might ask why we chose not to use an existing
+% termination prover for Haskell to discharge the termination
+% requirement. 
+% While certainly possible, we found that encoding the
+% termination proof via refinements provided a synergy that would have
+% been impossible with an external tool like AProVe. Consider the
+% following program:
+% %
+% \begin{code}
+%   -- countDown :: Nat -> Int
+%   countDown 0 = 0
+%   countDown n = countDown (n - 1)
+% \end{code}
+% %
+% We include the type as a comment to show the intended usage. A
+% TRS-based oracle will (correctly) say that @countDown@ may not
+% terminate, it could be called with a \emph{negative} input! Suppose,
+% however, that @countDown@ is only called with @Nat@s. \toolname will
+% then \emph{infer} the commented-out type, which will allow it to prove
+% that @countDown@ does, in fact, terminate on all \emph{provided}
+% inputs. The distinction between terminating on all possible vs.\ all
+% actual inputs is crucial for us since we are only concerned with
+% termination insofar as it allows us to prove safety properties.
+
+%%\spara{Testing}
+%%QuickCheck~\cite{quickcheck} is an automatic random testing tool
+%%for Haskell programs.
+%%%
+%%Compared to numerous existing static contract checkers, 
+%%testing fails to provide a
+%%complete correctness proof of a Haskell program, 
+%%but is tremendously easier to use.
+%%%
+%%The heavy usage of QuickCheck by the haskell programmers
+%%shows that 
+%%users do care for verification of their code,
+%%but are reluctant to spend much time
+%%to get complete correctness proof.
+%%%
+%%Combining testing and proving 
+%%(as in~\cite{Dybjer03}) would be ideal.
+%%%
+%%%%In an attempt to simplify correctness proves ~\citep{Dybjer03} 
+%%%%leaves some lemmas to be tested only.
+%%%
+%%One can directly translate  
+%%a QuickCheck property
+%%to a Haskell function that proves its correctness (\ref{sec:xmonad}).
+%%%
+%%We envision that \toolname 
+%%will be able to completely prove 
+%%a great number of QuickCheck properties 
+%%with a minimum effort from the user.
+%%
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "main"
+%%% End: 

research_exam @ 44d4674c

+Subproject commit 44d4674c4b258d7ad49f6e17753716e6b5b6bf81

results.tex

+\begin{table*}[ht!]
+\begin{scriptsize}
+\centering
+\begin{tabular}{|l|r|rrr|rrr|r|}
+\hline
+\textbf{Module} &\textbf{Version}           & \textbf{LOC} & \textbf{Mod} & \textbf{Fun} & \textbf{Specs} & \textbf{Annot} & \textbf{Qualif} & \textbf{Time (s)}\\
+\hline\hline
+\textsc{GHC.List} &      {7.4.1}    & 309          & 1            & 66           & 29 / 38        & 6 / 6          & 0 / 0           & 15 \\
+\textsc{Data.List} &    {4.5.1.0}    & 504          & 1            & 97           & 15 / 26        & 6 / 6          & 3 / 3           & 11 \\
+\hline
+\textsc{Data.Map.Base} &   {0.5.0.0} & 1396         & 1            & 180          & 125 / 173      & 13 / 13        & 0 / 0           & 174 \\
+\hline
+\textsc{Data.Set.Splay} &  {0.1.1} & 149          & 1            & 35           & 27 / 37        & 5 / 5          & 0 / 0           & 27 \\
+\hline
+\textsc{HsColour} &{1.20.0.0}          & 1047         & 16           & 234          & 19 / 40        & 5 / 5          & 1 / 1           & 196 \\
+\hline
+\textsc{XMonad.StackSet} & {0.11}  & 256          & 1            & 106          & 74 / 213       & 3 / 3          & 4 / 4           & 27 \\
+\hline
+\textsc{ByteString} &    {0.9.2.1}   & 3505         & 8            & 569          & 307 / 465      & 55 / 55        & 47 / 124        & 294 \\
+\hline
+\textsc{Text}        &    {0.11.2.3}  & 3128         & 17           & 493          & 305 / 717      & 52 / 54        & 49 / 97         & 499 \\
+\hline
+\textsc{Vector-Algorithms}& {0.5.4.2} & 1218         & 10           & 99           & 76 / 266       & 9 / 9          & 13 / 13         & 89 \\
+\hline
+\textbf{Total}            & & 11512        & 56           & 1879         & 977 / 1975     & 154 / 156      & 117 / 242       & 1336 \\
+\hline
+\end{tabular}
+\caption{\small A quantitative evaluation of our experiments. 
+  \textbf{Version} is version of the checked library.
+  \textbf{LOC} is the number of non-comment lines of source code as reported by \texttt{sloccount}.
+  \textbf{Mod}    is the number of modules in the benchmark and \textbf{Fun} is the number
+                  of functions.
+  \textbf{Specs}  is the number (/ line-count) of type specifications and aliases,
+                  data declarations, and measures provided.
+  \textbf{Annot}  is the number (/ line-count) of other annotations provided,
+                  these include invariants and hints for
+                  the termination checker.
+  \textbf{Qualif} is the number (/ line-count) of provided qualifiers.
+  \textbf{Time (s)}   is the time, in seconds, required to run \toolname. }
+\label{table:results}
+\end{scriptsize}
+\end{table*}

reviews.txt

+----------------------- REVIEW 1 ---------------------
+PAPER: 26
+TITLE: LiquidHaskell: Refinement Types in the Real World
+AUTHORS: Niki Vazou, Eric L. Seidel and Ranjit Jhala
+
+OVERALL EVALUATION: 2 (strong accept)
+REVIEWER'S CONFIDENCE: 4 (high)
+
+----------- REVIEW -----------
+Liquid types provide a lightweight mechanism for expressing contracts and other logical properties, including termination and totality, within Haskell. These types can be verified automatically, by means of SMT solving.
+
+The paper can be seen as a companion to the ICFP'14 paper "Refinement types for Haskell", which covers the theory of the approach. This paper covers a number of examples, as well as giving a general introduction to the approach. It also covers (in common with the ICFP paper) a set of benchmark results and related work. The paper is well written, and gives a set of well chosen examples.
+
+One piece of terminology is puzzling: measure is introduced as something that gives the size of a value, but it is later used for more general properties e.g. almostRB over red-black trees.
+
+The emphasis on integer values is also apparent in the predicate for non-emptiness for lists, which is expressed by saying that its length is greater than zero. Some rationale for this would be useful.
+
+Sections 3 and 4 cover "totality" and "termination" respectively. It would be helpful to explain these terms at the start of section 3, so that the two are distinguished appropriately.
+
+
+----------------------- REVIEW 2 ---------------------
+PAPER: 26
+TITLE: LiquidHaskell: Refinement Types in the Real World
+AUTHORS: Niki Vazou, Eric L. Seidel and Ranjit Jhala
+
+OVERALL EVALUATION: -1 (weak reject)
+REVIEWER'S CONFIDENCE: 3 (medium)
+
+----------- REVIEW -----------
+Summary:
+
+This paper presents LiquidHaskell, a implementation of Haskell
+extended with refinement types.  In particular, LiquidHaskell is a
+refinement type checker that can be run on a Haskell source program
+augmented with refinement type annotations and will report whether the
+program meets the specification given by the refinement types.  The
+paper gives a tour of features of the language, with a detailed
+discussion of the kinds of properties that it is possible to verify
+with refinement types, what kinds of annotations are necessary, and
+how one can go about verifying rich properties of Haskell programs,
+such as memory safety, with the LiquidHaskell system.
+
+Pros:
+
+I found this paper to be an engaging and pleasant read.  The
+example-driven approach does a great job of illustrating what's
+possible with LiquidHaskell (and quite a lot is possible).  The
+examples were clear and easy to follow, and from reading the paper I
+gained a better understanding both of the LiquidHaskell system and of
+refinement types in general.
+
+Cons:
+
+The main flaw I see with the paper as it stands is that it does not
+make clear what the relationship of this work is to the authors'
+related paper appearing in ICFP '14, and what the novelty of this
+paper is in comparison to it.  For instance, the evaluation section of
+this paper duplicates some of the evaluation section in the ICFP '14
+paper.
+
+Although I enjoyed reading the paper, I'm not sure that it is enough
+of a research contribution on its own.  However, I think it could be
+successfully recast as an experience report.
+
+The paper is also missing any discussion of how the LiquidHaskell type
+checker itself is implemented.
+
+Minor presentational issues:
+
+  * I wondered what "measures" were when they were mentioned at the
+    start of section 2; consider at least adding a forward reference
+    to section 2.3.
+
+  * Although the abstract mentions "a combination of refinement types
+    and SMT solvers", the paper never mentions SMT solvers again
+    except for a brief mention of Z3 in passing on page 9 and in the
+    related work on page 11.
+
+
+----------------------- REVIEW 3 ---------------------
+PAPER: 26
+TITLE: LiquidHaskell: Refinement Types in the Real World
+AUTHORS: Niki Vazou, Eric L. Seidel and Ranjit Jhala
+
+OVERALL EVALUATION: 1 (weak accept)
+REVIEWER'S CONFIDENCE: 4 (high)
+
+----------- REVIEW -----------
+This paper is a pleasing overview of the practical use of Liquid Haskell to verify large, real programs.
+
+Overall, I think this is a wonderful contribution to the Symposium.  My only concern is that the paper appears to be mostly an experience report (is this true?).  If so, I would appreciate a little more high-level guidance and advice for non-experts to use LH.  For example, are there lessons learned in debugging the (not-so-friendly) SMT output?  Is there anything you couldn't verify (e.g., libraries that use non-linear arithmetic or alternating quantifiers in the specifications?  If not, why?
+
+I think LH might give us a road map to have a verified set of base libraries for Haskell, which is quite an achievement no other mainstream language!
+
+Minor comments:
+
+- It appears this paper is an experience report, and I encourage the authors to mark it as such.
+
+- "we see that the output type is essentially" Can you add a footnote why it's not this type exactly?
+
+- "global in that, LIQUIDHASKELL" --> no comma
+
+- You mention that totality checks are w.r.t. Core.  Are errors then also w.r.t. Core?
+
+- "This case study illustrates an advantage of LIQUIDHASKELL over specialized provers (e.g., catch)" --> can you provide a reference for catch?
+
+- Before discussing HsColour, I'd give a brief explanation of what it is.
+
+- For memory safety verification, do you have some sort of model of the runtime that you're using?  More generally, can you describe in more detail your approach to reasoning about non-pure code?
+
+- Regarding your XMonad experience, you might want to compare your approach to the work of Wouter Swierstra: "Xmonad in Coq (Experience Report)".
+
+
+----------------------- REVIEW 4 ---------------------
+PAPER: 26
+TITLE: LiquidHaskell: Refinement Types in the Real World
+AUTHORS: Niki Vazou, Eric L. Seidel and Ranjit Jhala
+
+OVERALL EVALUATION: 2 (strong accept)
+REVIEWER'S CONFIDENCE: 3 (medium)
+
+----------- REVIEW -----------
+This paper describe the basics of LiquidHaskell (LH) and the authors' experience using LH to prove properties of several, mostly popular, libraries in the Haskell ecosystem.  LH leverages programmer-supplied annotations and type inferences to produce terms for an SMT solver, Z3 in this case, which indicate the presence or absence of program properties.
+
+Much to the authors credit, though I've only lightly followed LH and refinement types this paper explained the critical features in a digestible manner.  However, the limitations of the general approach and tool in particular were more nebulous and less explicit.  Example surprising or grey areas include the inability to verify aspects of HsColour and exactly what the termination checker might say about code consuming finite portions of infinite streams (ex: `take n (map f [1..])`).  Also, an explanation of the amount of effort needed to verify termination of the 33% of functions for which default measures did not suffice would be welcome.
+
+Given that verification of functional properties is the most immediately applicable section it is good to see real libraries considered.  It comes as a bonus that XMonad has already been formalized and properties proven in Coq, but the paper failed to capitalize by making any sort of statements contrasting the properties proven or expertise necessary for each verification - the question wasn't even acknowledged nor the prior work cited.
+
+Overall, the paper was strong in specific constructs and experience when the tool is applied to already-proven libraries by expert users.  The paper would be even more useful if it could communicate the boundary of what is achievable, further reveal developer benefits in terms of bug finding or productivity (vs mostly validating pre-existing correctness properties), and identify experiences that required intimate knowledge of LH internals (if any).
+
+Ignoring practical engineering matters, the applicability of LH to a project or problem is determined both by what the tool can do and by its limitations.  These two aspects bisect problems, cleanly or not, into those for which LH is a good fit and others.  Unless shortcomings are stated more explicitly it will remain hard for readers to understand when LH is a good fit for a particular problem.
+
+Nits:
+
+Abstract: The total line count is less interesting than the complexity of the properties and the complexity of the code base.  This is hard to quantify, but the single largest code base is a better estimate and the ranges of LOC and annotation count is even more informative.
+
+1. Introduction: The definition of div is more restrictive than Prelude.div, this was mildly distracting.  While the example annotated type is instructive I can't help but feel a better example exists.
+
+The document is not intended to describe the structure of LH, however many develops with correctness concerns continue to pick and choose their underlying prover carefully.  Whether or not the SMT solver is interchangeable interests audiences likely to put LH into practice.
+
+2. LiquidHaskell
+
+*Input* Item 2:  "a set of directories containing imported modules"
+
+Doesn't this present a scaling issue?  More complex code management and build systems resulting in a less useful tool?
+
+2.2 Verification
+
+"If we replace the <= with a <" ...
+
+Specifically, "the second <=".  There are two.
+
+7. Discussion
+Call out more of the weaknesses of the system.
+
+* When applying LiquidHaskell to a given library were any improvements to the tool necessary to complete the analysis, or was the tool sufficiently complete such that other users (not the maintainers) could have performed the same analysis?
+
+* How practical is organizing and keeping source copies of all imported modules?
+
+* When writing code, how can a developer know what constructs will present verification difficulties of the sort in HsColour?

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}

totality_numbers.tex

+catch vs totality:
+catch checked an really older version of hscolour with 4 patErrors.
+The current version has 7 
+which are different from the 4 checked by catch and fixed.
+
+
+measure definitions required: 2	
+data refined: 0
+refined top-level signatures:	9
+
+filename & total functions & typeErrors & patError & irrefutPatError & noMethidBindingError
+Data.Map.Base & 169 & 6 & 7 & 0 & 0
+XMonad.StackSet^[1] & 91 & 1& 0 4 & 0
+
+
+HsColour  & 242 & 7 & 13 & 1 & 1
+
+HsColour.hs & 13 & 2 & 3 & 0  & 0
+Language.Haskell.HsColour.hs & 10 & 0 & 0 & 0 & 0
+
+
+Language.Haskell.HsColour.ACSS.hs & 38 & 2 & 2 & 1 & 0 
+Language.Haskell.HsColour.Anchors.hs & 16 & ??(0) & 0 & 0 & 0 
+Language.Haskell.HsColour.ANSI.hs & 29& 1 & 0 & 0 & 1
+Language.Haskell.HsColour.Classify.hs & 19&??(2) & 2 & 0 & 0
+Language.Haskell.HsColour.ColourHighlight.hs &22 & 0 & 0 & 0 & 0
+Language.Haskell.HsColour.Colourise.hs & 28& 0 & 0 & 0 & 0
+Language.Haskell.HsColour.CSS.hs &7& & 0 & 0 & 0 & 0
+Language.Haskell.HsColour.General.hs & 2& 0 & 0 & 0 & 0
+Language.Haskell.HsColour.HTML.hs & 18& 0 & 0 & 0 & 0
+Language.Haskell.HsColour.InlineCSS.hs & 13 & 0 & 0 & 0 & 0
+Language.Haskell.HsColour.LaTeX.hs & 9& 0 & 0 & 0 & 0
+Language.Haskell.HsColour.MIRC.hs &10 & 1 & 6 & 0	 & 0
+Language.Haskell.HsColour.Options.hs & 4& 0 & 0 & 0 & 0
+Language.Haskell.HsColour.Output.hs & 16& 0 & 0 & 0 & 0
+Language.Haskell.HsColour.TTY.hs & 4& 0 & 0 & 0 & 0
+
+[1] :: 3 patterns automatically proved (x:xs) = reverse y:ys
\ No newline at end of file