\documentclass[11pt,a4paper,parskip=half]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb}
\usepackage[only,bigsqcap]{stmaryrd}

\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}

\usepackage{amsmath}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{tikz}
\usepackage{mathpartir}
\usepackage{calc}
\usepackage{booktabs}
\usepackage{longtable}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theorys in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

% Isabelle does not like *} in a text {* ... *} block
% Concrete implemenation thanks to http://www.mrunix.de/forums/showpost.php?p=235085&postcount=5
\newenvironment{alignstar}{\csname align*\endcsname}{\csname endalign*\endcsname}
\newenvironment{alignatstar}{\csname alignat*\endcsname}{\csname endalignat*\endcsname}

% quench koma warnings
\def\bf{\normalfont\bfseries}
\def\it{\normalfont\itshape}
\def\rm{\normalfont}
\def\sc{\normalfont\scshape}

% from http://tex.stackexchange.com/a/12931
\begingroup
  \catcode`\_=\active
  \gdef_#1{\ensuremath{\sb{\mathrm{#1}}}}
\endgroup
\mathcode`\_=\string"8000
\catcode`\_=12

\begin{document}

\title{The Safety of Call Arity}
\author{Joachim Breitner\\
Programming Paradigms Group\\
Karlsruhe Institute for Technology\\
\url{breitner@kit.edu}}
\maketitle


\begin{abstract}
We formalize the Call Arity analysis \cite{tfp}, as implemented in GHC, and prove both functional correctness and, more interestingly, safety (i.e.\ the transformation does not increase allocation). A highlevel overview of the work can be found in \cite{call-arity-haskell15}.

We use syntax and the denotational semantics from an earlier work \cite{breitner2013}, where we formalized Launchbury's natural semantics for lazy evaluation \cite{launchbury}. 
The functional correctness of Call Arity is proved with regard to that denotational semantics.
The operational properties are shown with regard to a small-step semantics akin to Sestoft's mark 1 machine \cite{sestoft}, which we prove to be equivalent to Launchbury's semantics.

We use Christian Urban's Nominal2 package \cite{nominal} to define our terms and make use of Brian Huffman's HOLCF package for the domain-theoretical aspects of the development \cite{holcf}.

\end{abstract}

\section*{Artifact correspondence table}
\label{sec:table}

The following table connects the definitions and theorems from \cite{call-arity-haskell15} with their corresponding Isabelle concept in this development.

\newcommand{\seetheory}[1]{\hyperref[sec_#1]{#1}}

\begin{center}
\begin{longtable}[h]{lll}
\textsf{Concept} & \textsf{corresponds to} & \textsf{in theory} \\
\midrule
Syntax                                                        & \isacommand{nominal-datatype} \isa{expr}                  & Terms in \cite{breitner2013} \\
Stack                                                         & \isacommand{type-synonym} \isa{stack}                     & \seetheory{SestoftConf} \\
Configuration                                                 & \isacommand{type-synonym} \isa{conf}                      & \seetheory{SestoftConf} \\
Semantics ($\Rightarrow$)                                     & \isacommand{inductive} \isa{step}                         & \seetheory{Sestoft} \\
Arity                                                         & \isacommand{typedef} \isa{Arity}                          & \seetheory{Arity} \\
Eta-expansion                                                 & \isacommand{lift-definition} \isa{Aeta-expand}            & \seetheory{ArityEtaExpansion} \\
Lemma 1                                                       & \isacommand{theorem} \isa{Aeta-expand-safe}            & \seetheory{ArityEtaExpansionSafe} \\
$\mathcal A_\alpha(\Gamma, e)$                                & \isacommand{locale} \isa{ArityAnalysisHeap}               & \seetheory{ArityAnalysisSig} \\
$\mathsf T_\alpha(e)$                                         & \isacommand{sublocale} \isa{AbstractTransformBound}       & \seetheory{ArityTransform} \\
$\mathcal A_\alpha(e)$                                        & \isacommand{locale} \isa{ArityAnalysis}                   & \seetheory{ArityAnalysisSig} \\
Definition 2                                                  & \isacommand{locale} \isa{ArityAnalysisLetSafe}         & \seetheory{ArityAnalysisSpec} \\
Definition 3                                                  & \isacommand{locale} \isa{ArityAnalysisLetSafeNoCard}   & \seetheory{ArityAnalysisSpec} \\
Definition 4                                                  & \isacommand{inductive} \isa{a-consistent}                 & \seetheory{ArityConsistent} \\
Definition 5                                                  & \isacommand{inductive} \isa{consistent}                   & \seetheory{ArityTransformSafe} \\
Lemma 2                                                       & \isacommand{lemma} \isa{arity-transform-safe}             & \seetheory{ArityTransformSafe} \\
% Concrete arity analysis                                     & \isacommand{definition} \isa{Real-Aexp}                   & \seetheory{ArityAnalysisImpl} \\
$\operatorname{Card}$                                         & \isacommand{type-synonym} \isa{two}                       & \seetheory{Cardinality-Domain} \\
$\mathcal C_\alpha(\Gamma, e)$                                & \isacommand{locale} \isa{CardinalityHeap}                 & \seetheory{CardinalityAnalysisSig} \\
$\mathcal C_{(\bar\alpha,\alpha,\dot\alpha)}((\Gamma, e, S))$ & \isacommand{locale} \isa{CardinalityPrognosis}            & \seetheory{CardinalityAnalysisSig} \\
Definition 6                                                  & \isacommand{locale} \isa{CardinalityPrognosisSafe}     & \seetheory{CardinalityAnalysisSpec} \\
Definition 7 ($\Rightarrow_\#$)                               & \isacommand{inductive} \isa{gc-step}                      & \seetheory{SestoftGC} \\
Definition 8                                                  & \isacommand{inductive} \isa{consistent}                   & \seetheory{CardArityTransformSafe} \\
Lemma 3                                                       & \isacommand{lemma} \isa{card-arity-transform-safe}        & \seetheory{CardArityTransformSafe} \\
Trace trees                                                   & \isacommand{typedef} \isa{'a ttree}                       & \seetheory{TTree} \\
Function $s$                                                  & \isacommand{lift-definition} \isa{substitute}             & \seetheory{TTree} \\
$\mathcal T_\alpha(e)$                                        & \isacommand{locale} \isa{TTreeAnalysis}                   & \seetheory{TTreeAnalysisSig} \\
$\mathcal T_\alpha(\Gamma,e)$                                 & \isacommand{locale} \isa{TTreeAnalysisCardinalityHeap}    & \seetheory{TTreeAnalysisSpec} \\
Definition 9                                                  & \isacommand{locale} \isa{TTreeAnalysisCardinalityHeap}    & \seetheory{TTreeAnalysisSpec} \\
Lemma 4                                                       & \isacommand{sublocale} \isa{CardinalityPrognosisSafe}  & \seetheory{TTreeImplCardinalitySafe} \\
Co-Call graphs                                                & \isacommand{typedef} \isa{CoCalls}                        & \seetheory{CoCallGraph} \\
Function $g$                                                  & \isacommand{lift-definition} \isa{ccApprox}               & \seetheory{CoCallGraph-TTree} \\
Function $t$                                                  & \isacommand{lift-definition} \isa{ccTTree}                & \seetheory{CoCallGraph-TTree} \\
$\mathcal G_\alpha(e)$                                        & \isacommand{locale} \isa{CoCallAnalysis}                  & \seetheory{CoCallAnalysisSig} \\
$\mathcal G_\alpha(\Gamma, e)$                                & \isacommand{locale} \isa{CoCallAnalysisHeap}              & \seetheory{CoCallAnalysisSig} \\
Definition 10                                                 & \isacommand{locale} \isa{CoCallAritySafe}              & \seetheory{CoCallAnalysisSpec} \\
Lemma 5                                                       & \isacommand{sublocale} \isa{TTreeAnalysisCardinalityHeap} & \seetheory{CoCallImplTTreeSafe} \\
Call Arity & \isacommand{nominal-function} \isa{cCCexp}                & \seetheory{CoCallAnalysisImpl} \\
Theorem 1                                                     & \isacommand{lemma} \isa{end2end-closed}                   & \seetheory{CallArityEnd2EndSafe} \\
\end{longtable}
\end{center}

\bibliographystyle{amsalpha}
\bibliography{\jobname}

\tableofcontents
\newcommand{\theory}[1]{\subsection{#1}\label{sec_#1}\input{#1.tex}}

%\let\OldInput\input
%\renewcommand{\input}[1]{{
%        \subsection{#1}
%        \OldInput{#1}
%}}

%\OldInput{session.tex}


\section{Various Utilities}

\theory{ConstOn}
\theory{Set-Cpo}
\theory{Env-Set-Cpo}
\theory{AList-Utils-HOLCF}
\theory{List-Interleavings}



\section{Small-step Semantics}
\theory{SestoftConf}
\theory{Sestoft}
\theory{SestoftGC}
\theory{BalancedTraces}
\theory{SestoftCorrect}

\section{Arity}
\theory{Arity}
\theory{AEnv}
\theory{Arity-Nominal}
\theory{ArityStack}

\section{Eta-Expansion}

\theory{EtaExpansion}
\theory{EtaExpansionSafe}
\theory{TransformTools}
\theory{ArityEtaExpansion}
\theory{ArityEtaExpansionSafe}

\section{Arity Analysis}

\theory{ArityAnalysisSig}
\theory{ArityAnalysisAbinds}
\theory{ArityAnalysisSpec}
\theory{TrivialArityAnal}
\theory{ArityAnalysisStack}

\theory{ArityAnalysisFix}
\theory{ArityAnalysisFixProps}

\section{Arity Transformation}

\theory{AbstractTransform}
\theory{ArityTransform}


\section{Arity Analysis Safety (without Cardinality)}
\theory{ArityConsistent}
\theory{ArityTransformSafe}

\section{Cardinality Analysis}

\theory{Cardinality-Domain}
\theory{CardinalityAnalysisSig}
\theory{CardinalityAnalysisSpec}

\theory{NoCardinalityAnalysis}

\theory{CardArityTransformSafe}

\section{Trace Trees}
\theory{TTree}
\theory{TTree-HOLCF}

\section{Trace Tree Cardinality Analysis}
\theory{AnalBinds}
\theory{TTreeAnalysisSig}
\theory{Cardinality-Domain-Lists}
\theory{TTreeAnalysisSpec}
\theory{TTreeImplCardinality}
\theory{TTreeImplCardinalitySafe}


\section{Co-Call Graphs}
\theory{CoCallGraph}
\theory{CoCallGraph-Nominal}

\section{Co-Call Cardinality Analysis}

\theory{CoCallAnalysisSig}
\theory{CoCallAnalysisBinds}
\theory{CoCallAritySig}
\theory{CoCallAnalysisSpec}
\theory{CoCallFix}

\theory{CoCallGraph-TTree}
\theory{CoCallImplTTree}
\theory{CoCallImplTTreeSafe}

\section{CoCall Cardinality Implementation}
\theory{CoCallAnalysisImpl}
\theory{CoCallImplSafe}

\section{End-to-end Saftey Results and Example}
\theory{CallArityEnd2End}
\theory{CallArityEnd2EndSafe}

\section{Functional Correctness of the Arity Analysis}
\theory{ArityAnalysisCorrDenotational}

%%% Local Variables:
%%% mode: l
%%% TeX-master: "root"
%%% End:

\end{document}
