\documentclass{jfp1}
\usepackage{graphicx}
\usepackage{style/utils}
\usepackage{style/names}
\usepackage{style/proof}


% -----------------------------------------------------------------------------
\begin{document}

\title	[Witnessing Mutability, Purity and Aliasing for Program Optimisation]
	{Witnessing Mutability, Purity and Aliasing \\ for Program Optimisation}

\author	[Ben Lippmeier]
	{  BEN LIPPMEIER \\
	   School of Computer Science and Engineering \\
	   University of New South Wales, Australia
	   \email{benl@ouroborus.net}
	}

\maketitle


% -- Abstract -----------------------------------------------------------------
\begin{abstract}
Restricting destructive update to values of a distinguished reference type prevents functions from being polymorphic in the mutability of their arguments. This restriction makes it easier to reason about program behaviour during transformation, but the lack of polymorphism reduces the expressiveness of the language. We present a System-F style core intermediate language that uses dependently kinded proof witnesses to encode information about the mutability and aliasing properties of data, and the purity of computations. We support mixed strict and lazy evaluation, and use our type system to ensure that only computations without visible side effects are suspended.
\end{abstract}


\input{01-Intro}
\input{02-Update}
\input{03-Witness}
\input{04-Language}

\clearpage{}
\input{05-Properties}

\clearpage{}
\input{06-Floating}

\clearpage{}
\input{07-Hoisting}

\clearpage{}
\input{08-Distinctness}

\clearpage{}
\input{09-Comparisons}
\input{10-Conclusion}

\bibliography{Main.bib}
\bibliographystyle{jfp}

\end{document}

