\documentclass[conference]{IEEEtran}

\usepackage[cmex10]{amsmath}
\usepackage{url}
\usepackage{listings}

\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  numbers=left,
  stepnumber=1,
  numberstyle={\scriptsize},
  numbersep=1em,
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  escapechar={@},
}

\ifCLASSINFOpdf
  % \usepackage[pdftex]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../pdf/}{../jpeg/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.pdf,.jpeg,.png}
\else
  % or other class option (dvipsone, dvipdf, if not using dvips). graphicx
  % will default to the driver specified in the system graphics.cfg if no
  % driver is specified.
  % \usepackage[dvips]{graphicx}
  % declare the path(s) where your graphic files are
  % \graphicspath{{../eps/}}
  % and their extensions so you won't have to specify these with
  % every instance of \includegraphics
  % \DeclareGraphicsExtensions{.eps}
\fi


% correct bad hyphenation here
\hyphenation{op-tical net-works semi-conduc-tor}


\begin{document}
%
% paper title
% Titles are generally capitalized except for words such as a, an, and, as,
% at, but, by, for, in, nor, of, on, or, the, to and up, which are usually
% not capitalized unless they are the first or last word of the title.
% Linebreaks \\ can be used within to get better formatting as desired.
% Do not put math or special symbols in the title.
\title{Categorical Formalization of Program Modification}


% author names and affiliations
% use a multiple column layout for up to three different
% affiliations
\author{
\IEEEauthorblockN{Yasutaka HIGA}
\IEEEauthorblockA{University of the Ryukyus \\ Email: atton@cr.ie.u-ryukyu.ac.jp}
\and
\IEEEauthorblockN{Shinji KONO}
\IEEEauthorblockA{University of the Ryukyus \\ Email: kono@ie.u-ryukyu.ac.jp}
}

% make the title area
\maketitle

% As a general rule, do not put math, special symbols or citations
% in the abstract
\begin{abstract}
The abstract goes here.
\end{abstract}

% no keywords




% For peer review papers, you can put extra information on the cover
% page as needed:
% \ifCLASSOPTIONpeerreview
% \begin{center} \bfseries EDICS Category: 3-BBND \end{center}
% \fi
%
% For peerreview papers, this IEEEtran command inserts a page break and
% creates the second title. It will be ignored for other modes.
\IEEEpeerreviewmaketitle

\section{Continuation based C}  % enough only describe code/data segment?
We proposed programming style using unit of program named code segment and data segment. % TODO: ref
Code segment is a unit of calculation not dependents state.
Data segment contains values of calculation and calculation context called meta data segment.
Execution of program is represented by moves interconnected code segments.
Code/Data segment style programming was suitable to state based concurrent program.

Programming language 'Continuation based C' (CbC) supported code/data segment style programming. % TODO: ref
CbC is lower language of C removed function call and loop-statements(for, while) and added continuation by goto and code segment.
Code segment of CbC is function without return values in C.
Interconnections of code segment represents goto with environment.
CbC can define meta calculation as calculation of calculation named meta code segment.
Meta computations contains various computations including partiality, nondeterminism, side-effects, exceptions and continuations.

\section{Meta computation and Monads}
Meta computations in CbC formalized by Monads to prevent chaos by unlimited computations.
Monads are a notion of Category Theory, in programs Monad correspondence of normal/meta computations.
For example, diverging computation as extended normal computations is represented direct sum of normal values and bottom.

We show formalization of programs for using Monads.
Programs notated typed lambda calculus constructed values and abstractions.
Abstraction f maps value to value, and applies to value x notated $ f x $.
Every lambda term has a type.
Value x has type A notated $ x : A $.
Abstraction f has a argument of type A and return value of type B notated $ f : A \rightarrow B $.

\begin{eqnarray*}
    x : A \\
    f : A \rightarrow B \\
    f x : B \\
\end{eqnarray*}

Type matched abstractions can be composed by operator ';'.
Order of composition are commutative.

\begin{eqnarray*}
    f : A \rightarrow B \\
    g : B \rightarrow C \\
    f;g : A \rightarrow C \\
    \\
    h : C \rightarrow D \\
    (f;g);h = f;(g;h)
\end{eqnarray*}

Abstractions has many arguments notated by abstraction took a argument, and returns a abstraction that argument numbers has decreased(Currying).

Abstractions can be extended using Monad.
Monad is $ triple (T, \eta, \mu) $ satisfies laws(Figure) % TODO :commutative diagram
Various meta computations represents by definition of triple.
Monad has another description Kleisli Triple $ (T, \eta, \_^{*}) $.

Kleisli triple are following equations hold:

\begin{itemize}
    \item $ \eta^{*}_A    = id_{T A} $
    \item $ \eta;f^{*}    = f \mbox{ for } f : A \rightarrow T B $
    \item $ f^{*} ; g^{*} = (f; g^{*})^{*} \mbox{ for } f : A \rightarrow T B \mbox{ and } g : B \rightarrow T C $
\end{itemize}

$ id $ is abstraction that identity mapping for any typed values ($ id x = x $).
$ id $ was exists any typed values.
Notation $ id_{X} x $ is application $ id $ to a value x typed X.
Then, $ T $ is functor that pair of structure and a map that abstraction for non-structured values to abstraction for structured values.
If applied functor T to type A notated $ T A $.
For example, list of any types is functor.
List can be constructed to any typed values (list of characters, list of integers, etc) and can be apply abstraction for stored elements.

\begin{eqnarray*}
    xs = \verb/[10 , 20 , 30]/ \\
    xs : \verb/List Int/ \\
    f  : \verb/Int/ \rightarrow \verb/String/ \\
    \verb/[f 10 , f 20 , f 30]/ : \verb/List String/
\end{eqnarray*}

It's summarized informal definition of functor for explain Monad.
Values extended using property of functor T extend abstraction to normal values to structured values.
Kleisli triple $ (T, \eta, \_^{*}) $ are a triple of functor T and $ \eta $ extension of normal values to meta one and $ \_^{*} $ extension of abstraction.
Kleisli triple are derivable from Monad $ (T, \eta, \mu) $

Definition of diverging computation as extend normal computations using Monad are shown.

\begin{itemize}
    \item $ T A = A_{\bot} (= A + \{\bot\}) $
    \item $ \eta_A $ is the inclusion of A into $ A_{\bot} $
    \item if $ f : A \rightarrow T B $, then $ f^{*} (\bot) = \bot $ and $ f^{*}(a) = f (a) $ when $ a $  has type A.
\end{itemize}

\section{Modification of Program using Monad}
Reliability of a program dynamically changed in software development.
We propose handle modifications of a program as meta computations for improve reliability.
Modifications represents a set of program versions including values and abstraction with type consistency.
Execution of program including modification like concurrent execution of all versions.

Definition of modifications named 'Delta Monad' are shown:

\begin{itemize}
    \item $ T A = A_0 \times A_1 \times \dots \times A_n $
    \item $ \eta_A $ is map to values accumulated modification.
    \item if $ f : A \rightarrow T B $ and $ x : T A  $ then \\
        $ f^{*}(x) = \langle f_0(x_0) , f_1(x_1), \dots, f_n(x_n) \rangle$
\end{itemize}

Versions of a program without branching represents finite direct product.

We simulated Delta Monad in Haskell (Table\ref{src:delta_monad}).

\begin{table}[html]
\begin{lstlisting}
data Delta a = Mono a | Delta a (Delta a)

headDelta :: Delta a -> a
headDelta (Mono  x)   = x
headDelta (Delta x _) = x

tailDelta :: Delta a -> Delta a
tailDelta (Mono x)     =  Mono x
tailDelta (Delta _ ds) = ds

instance Monad Delta where
  return x           = Mono x
  (Mono x) >>= f     = f x
  (Delta x d) >>= f  = Delta (headDelta (f x))
                             (d >>= (tailDelta . f))
\end{lstlisting}
    \label{src:delta_monad}
    \caption{Definition of Delta Monad in Haskell}
\end{table}

We aim to prove Delta Monads satisfies Monad laws using Haskell has built-in Monad definition.
Modifications of values stored list like structure named Delta.
Delta contains two constructor Mono and Delta, Mono represents first version, Delta represents modification.
Infix operator \verb/>>=/ handles extended abstraction has typed $ \verb/A/ \rightarrow \verb/Delta B/ $ recursive applies to each original versions.
This definition represents simple modification only monotonic increase versioning (exclude branching and merging) and program has consistent type in all versions.
We executed different versions in same time and proved satisfying Monad laws by proof assistant language Agda.

\section{Conclusion and Future Works}
Handleable modification by meta computations is proposed.
Using this Delta Monad, we can make reliable program development possible.
Especially, Automatically property comparison in development cycle is made possible by CbC also plans incorporate model checker as meta computations.
We aim to extend Delta Monad represents all possible modifications (branching, merging, and more) with proof and implement to CbC.


% An example of a floating figure using the graphicx package.
% Note that \label must occur AFTER (or within) \caption.
% For figures, \caption should occur after the \includegraphics.
% Note that IEEEtran v1.7 and later has special internal code that
% is designed to preserve the operation of \label within \caption
% even when the captionsoff option is in effect. However, because
% of issues like this, it may be the safest practice to put all your
% \label just after \caption rather than within \caption{}.
%
% Reminder: the "draftcls" or "draftclsnofoot", not "draft", class
% option should be used if it is desired that the figures are to be
% displayed while in draft mode.
%
%\begin{figure}[!t]
%\centering
%\includegraphics[width=2.5in]{myfigure}
% where an .eps filename suffix will be assumed under latex,
% and a .pdf suffix will be assumed for pdflatex; or what has been declared
% via \DeclareGraphicsExtensions.
%\caption{Simulation results for the network.}
%\label{fig_sim}
%\end{figure}

% Note that IEEE typically puts floats only at the top, even when this
% results in a large percentage of a column being occupied by floats.


% An example of a double column floating figure using two subfigures.
% (The subfig.sty package must be loaded for this to work.)
% The subfigure \label commands are set within each subfloat command,
% and the \label for the overall figure must come after \caption.
% \hfil is used as a separator to get equal spacing.
% Watch out that the combined width of all the subfigures on a
% line do not exceed the text width or a line break will occur.
%
%\begin{figure*}[!t]
%\centering
%\subfloat[Case I]{\includegraphics[width=2.5in]{box}%
%\label{fig_first_case}}
%\hfil
%\subfloat[Case II]{\includegraphics[width=2.5in]{box}%
%\label{fig_second_case}}
%\caption{Simulation results for the network.}
%\label{fig_sim}
%\end{figure*}
%
% Note that often IEEE papers with subfigures do not employ subfigure
% captions (using the optional argument to \subfloat[]), but instead will
% reference/describe all of them (a), (b), etc., within the main caption.
% Be aware that for subfig.sty to generate the (a), (b), etc., subfigure
% labels, the optional argument to \subfloat must be present. If a
% subcaption is not desired, just leave its contents blank,
% e.g., \subfloat[].


% An example of a floating table. Note that, for IEEE style tables, the
% \caption command should come BEFORE the table and, given that table
% captions serve much like titles, are usually capitalized except for words
% such as a, an, and, as, at, but, by, for, in, nor, of, on, or, the, to
% and up, which are usually not capitalized unless they are the first or
% last word of the caption. Table text will default to \footnotesize as
% IEEE normally uses this smaller font for tables.
% The \label must come after \caption as always.
%
%\begin{table}[!t]
%% increase table row spacing, adjust to taste
%\renewcommand{\arraystretch}{1.3}
% if using array.sty, it might be a good idea to tweak the value of
% \extrarowheight as needed to properly center the text within the cells
%\caption{An Example of a Table}
%\label{table_example}
%\centering
%% Some packages, such as MDW tools, offer better commands for making tables
%% than the plain LaTeX2e tabular which is used here.
%\begin{tabular}{|c||c|}
%\hline
%One & Two\\
%\hline
%Three & Four\\
%\hline
%\end{tabular}
%\end{table}


% Note that the IEEE does not put floats in the very first column
% - or typically anywhere on the first page for that matter. Also,
% in-text middle ("here") positioning is typically not used, but it
% is allowed and encouraged for Computer Society conferences (but
% not Computer Society journals). Most IEEE journals/conferences use
% top floats exclusively.
% Note that, LaTeX2e, unlike IEEE journals/conferences, places
% footnotes above bottom floats. This can be corrected via the
% \fnbelowfloat command of the stfloats package.




\section{Conclusion}
The conclusion goes here.




% conference papers do not normally have an appendix


% use section* for acknowledgment
\section*{Acknowledgment}


The authors would like to thank...





% trigger a \newpage just before the given reference
% number - used to balance the columns on the last page
% adjust value as needed - may need to be readjusted if
% the document is modified later
%\IEEEtriggeratref{8}
% The "triggered" command can be changed if desired:
%\IEEEtriggercmd{\enlargethispage{-5in}}

% references section

% can use a bibliography generated by BibTeX as a .bbl file
% BibTeX documentation can be easily obtained at:
% http://www.ctan.org/tex-archive/biblio/bibtex/contrib/doc/
% The IEEEtran BibTeX style support page is at:
% http://www.michaelshell.org/tex/ieeetran/bibtex/
%\bibliographystyle{IEEEtran}
% argument is your BibTeX string definitions and bibliography database(s)
%\bibliography{IEEEabrv,../bib/paper}
%
% <OR> manually copy in the resultant .bbl file
% set second argument of \begin to the number of references
% (used to reserve space for the reference number labels box)
\begin{thebibliography}{1}

\bibitem{IEEEhowto:kopka}
H.~Kopka and P.~W. Daly, \emph{A Guide to \LaTeX}, 3rd~ed.\hskip 1em plus
  0.5em minus 0.4em\relax Harlow, England: Addison-Wesley, 1999.

\end{thebibliography}




% that's all folks
\end{document}