--- a/delta.tex	Tue Feb 24 15:54:22 2015 +0900
+++ b/delta.tex	Thu Feb 26 17:57:31 2015 +0900
@@ -63,7 +63,7 @@
 
 \section{Formalization of Modifications}
 In software development, programs was modified for implementing features, refactoring, and more.
-But defective modifies decreases reliability of program.
+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.
@@ -74,6 +74,31 @@
 In this paper, We propose meta computation execute a program includes modifications simultaneously on Delta.
 Additionally, Delta Monad can be used with other Monads for more computations of modifications.
 
+\section{Programs and Monads}
+Programs notated typed lambda calculus constructed values and abstractions.
+Abstractions maps value to value.
+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}
+
+Execution of a program is application of abstraction.
+Some computations can not be notated abstraction like Input/Output are meta computation.
+Meta computations are computations for implements computations.
+
+
+
+\section{Definition of Delta Monad}
+\section{An example of program includes modification}
+\section{DeltaM combinator with other Monads}
+\section{An example of program includes modification with traces}
+\section{Conclusion and future works}
+
 \appendix
 \section{Appendix Title}