\documentclass[preprint]{sigplanconf}

% The following \documentclass options may be useful:

% preprint      Remove this option only once the paper is in final form.
% 10pt          To set in 10-point type instead of 9-point.
% 11pt          To set in 11-point type instead of 9-point.
% authoryear    To obtain author/year citation style instead of numeric.

\usepackage{amsmath}


\begin{document}

\special{papersize=8.5in,11in}
\setlength{\pdfpageheight}{\paperheight}
\setlength{\pdfpagewidth}{\paperwidth}

\conferenceinfo{ICFP '15}{August 31 - September 2 , 2015, Vancouver, British Columbia, Canada}
\copyrightyear{2015}
\copyrightdata{978-1-nnnn-nnnn-n/yy/mm}
\doi{nnnnnnn.nnnnnnn}

% Uncomment one of the following two, if you are not going for the
% traditional copyright transfer agreement.

%\exclusivelicense                % ACM gets exclusive license to publish,
                                  % you retain copyright

%\permissiontopublish             % ACM gets nonexclusive license to publish
                                  % (paid open-access papers,
                                  % short abstracts)

%\titlebanner{banner above paper title}        % These are ignored unless
\preprintfooter{Formalization of Program Modifications using Monad}   % 'preprint' option specified.

\title{Formalization of Program Modifications using Monad}

\subtitle{}

\authorinfo{Yasutaka HIGA}
           {Department of Information Engineering \\ University of the Ryukyus}
           {atton@cr.ie.u-ryukyu.ac.jp}
\authorinfo{Shiji KONO}
           {University of the Ryukyus}
           {kono@ie.u-ryukyu.ac.jp}

\maketitle

\begin{abstract}
This is the text of the abstract.
\end{abstract}

\category{CR-number}{subcategory}{third-level}

% general terms are not compulsory anymore,
% you may leave them out
\terms
term1, term2

\keywords
keyword1, keyword2

\section{Formalization of Modifications}
In software development, programs was modified for implementing features, refactoring, and more.
However, defective modifies decreases reliability of program.
Formalization of program modifications proposed to improves reliability.
Especially, We formalized modifications using Monad.
Monad provides notions of meta computations (partiality, nondeterminism, side-effects, ...) in functional program.
We define meta computation notated modifications list like structure named Delta Monad.

Delta Monad represents modifications by accumulates all versions of a program.
Accumulated modifications can computes by meta computation.
In this paper, We propose meta computation execute a program includes modifications simultaneously on Delta.

\section{Programs and Monads}
Programs notated typed lambda calculus constructed values and abstractions.
Abstractions maps value to value.
Abstraction f applies to 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 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}

Kleisli Triple can build from Monad ($ (T, \eta, \mu) $).

For Example, definition of diverging computation 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 using Monad}

\begin{equation*}
    T A = A_0 \times A_1 \times \dots \times A_n
\end{equation*}

\begin{eqnarray*}
    x : A \\
    x^{*} : T A \\
    x^{*} : A_0 \times A_1 \times \dots \times A_n \\
    \\
    f : A \rightarrow B \\
    f^{*} : A \rightarrow T B \\
    f^{*} : (A_0 \rightarrow B_0) \times (A_1 \rightarrow B_1) \times \dots \times (A_n \rightarrow B_n)
\end{eqnarray*}

\begin{eqnarray*}
    f^{*} : A \rightarrow T B \\
    f^{*} = f_0 \times f_1 \times \dots f_n \\
    \\
    g^{*} : B \rightarrow T C \\
    g^{*} = g_0 \times g_1 \times \dots g_n \\
    \\
    g^{*} \circ f^{*} : A \rightarrow T C \\
    g^{*} \circ f^{*} = (g_0 \circ f_0) \times (g_1 \circ f_1) \times \dots \times (g_n \circ f_n)
\end{eqnarray*}



\appendix
\section{Appendix Title}

This is the text of the appendix, if you need one.

\acks

Acknowledgments, if needed.

% We recommend abbrvnat bibliography style.

\bibliographystyle{abbrvnat}

% The bibliography should be embedded for final submission.

\begin{thebibliography}{}
\softraggedright

\bibitem[Smith et~al.(2009)Smith, Jones]{smith02}
P. Q. Smith, and X. Y. Jones. ...reference text...

\end{thebibliography}


\end{document}

%                       Revision History
%                       -------- -------
%  Date         Person  Ver.    Change
%  ----         ------  ----    ------

%  2013.06.29   TU      0.1--4  comments on permission/copyright notices