--- a/gears.ind	Tue May 12 04:07:34 2015 +0900
+++ b/gears.ind	Tue May 12 10:44:14 2015 +0900
@@ -2,17 +2,24 @@
 
 --abstract:
 
---Reliable computation and predictablity
+We introduce system of code and data. Instead of function call, code accepts input data and simply generates output data.
+Chains of code and data performs computation. After calling next code, it does not return to the caller, so it has no
+environment nor calling stack. This system is designed for reliable system description and parallel execution on various
+architecture. We use segments or gears sometime. This is directly connected to the category theory like lambda calculus.
+We also find a categorical representation from the view point of data. This shows duality of code and data. This duality will be
+a guideline of our system design.
 
-Various softwares are used in real world. Each of them have to work in a reliable way. A peice of devie contains
-millons of lines of code. These programs are written in C, Haskell and so on. 
+--Reliable computation and predictability
+
+Various software are used in real world. Each of them have to work in a reliable way. A piece of device contains
+millions of lines of code. These programs are written in C, Haskell and so on. 
 To assure its reliability, the computation of a function should be predictable.
-The correctness of the predecion should be assured by measurements, model checkings or proofs.
+The correctness of the prediction should be assured by measurements, model checking or proofs.
 
 % The unit of computation of conventional programming language is of course a function call.
 % a function may call another functions and it comes back to the original function. 
 % Proof theory such as Hoare Logic or model checking method is used to make the prediction, such as
-% zero divide is never occured in a function.
+% zero divide is never occurred in a function.
 
 We propose new unit of computation, data segments and code segments. Computations in these segments are finite and
 predictable. We sometimes call these gears. 
@@ -26,7 +33,7 @@
 
 --Definition of data segment and code segment
 
-Actually we implment our Gears language in LLVM\cite{LLVM}, but we can think both code and data are System F\cite{}  term. As usuall, Types are
+Actually we implement our Gears language in LLVM\cite{LLVM}, but we can think both code and data are System F\cite{Girard:1989:PT:64805}  term. As usual, Types are
 defined starting from type variables X,Y,Z and is generated by two operations:
 
     1. if U and V are types, then U → V is a type.
@@ -35,44 +42,48 @@
 Terms are constructed by six schemes
 
     1. variable: $x^T, y^T, z^T,...$ of type $T$,
-    2. application: $tu$ ov type $V$, where $t$ is of type $U→V$ and $u$ is of type $U$,
+    2. application: $tu$ of type $V$, where $t$ is of type $U→V$ and $u$ is of type $U$,
     3. λ-abstraction: $λx^U.v$ of type $U→V$, where $x^U$ is a variable of type $U$ and $v$ is of type $V$,
     4. universal abstraction: if $v$ is a term type V, then we can form $ΛX.v$ of type $ΠX.V$, so long as the variable $X$ is not free in the type of a free variable of $v$.
-    5. universal application: if $t$ is a term of type $ΠX.V$ and $U$ is a type, then %tU$ is a tem of type $V[U/X]$.
+    5. universal application: if $t$ is a term of type $ΠX.V$ and $U$ is a type, then %tU$ is a term of type $V[U/X]$.
 
-and usuall conversions,
+and usual conversions,
 
     1.  (λx.v)u 〜> v[u/x]
     2.  (ΛX.v)U 〜> v[U/X]
 
-Code segments of type $C$ accepts data segments of type $I$ and generates data segments of type $O$. 
+What we need here is that a term has a type, a function has type $U → V$.
+Code segments f of type $I → O$, accepts data segments of type $I$ and generates data segments of type $O$. 
 
-    C : I → O
+    f : I → O
 
-Domain of C is I and codemain of C is O.
+Domain of C is I and codomain of C is O. 
 
-<center><img src="fig/codeGear.jpg"></center>
+Gears system only allows calling another code at the bottom of the code, that is all codes have tail call form. Normal function call
+is not prohibited, but it should be closed in a code. 
+
+<center><img src="fig/codeGear.svg"></center>
 
 --Meta computation of Gears
 
-Computation of a code is limited in the inputs and the outputs and it makes the compuation of the code predictable, but its data are
-ususally connected to other data. The code has its continuation also. These connections are out of the scope of the code.
-We think these connections are made by a meta computation, such as monads\cite{}. A monad is a data structure with monad laws and
-after an execution of a code, monad's join code is called to handle meta data structure. With monad $T$, 
+Computation of a code is limited in the inputs and the outputs and it makes the computation of the code predictable, but its data are
+usually connected to other data. The code has its continuation also. These connections are out of the scope of the code.
+We think these connections are made by a meta computation, such as monads\cite{Moggi:1989:CLM:77350.77353}. A monad is a data structure with monad laws and
+after an execution of a code, monads join code is called to handle meta data structure. With monad $T$, 
 
     C' : I → T O
 
-is a meta compuation. $C$ has one to one correcpondence with $C'$.
+is a meta computation. $C$ has one to one correspondence with $C'$.
 
     μ : T (T O) → T O
 
-Parallel execution or IO handling are represented as a monad in our scheme. 
+Parallel execution or IO handling are represented as a monad in our scheme.  Monads are only allows to use at the bottom of a code in our system.
 
-<center><img src="fig/meta.jpg"></center>
+<center><img src="fig/meta.svg"></center>
 
---A cateogy of codes 
+--A category of codes 
 
-Types of code segments and  data segments narually compose a category of function and types. Codes and data are interconnected one by one.
+Types of code segments and  data segments naturally compose a category of function and types. Codes and data are interconnected one by one.
 
     Object : a, b, c  ...
     Arrows : f, g, h  ...
@@ -84,11 +95,11 @@
     g : b → c
     f : c → d
 
-There is compositon of arrows,
+There is composition of arrows,
 
     f o g : b → d
 
-and it satisfies the compisition law.
+and it satisfies the composition law.
 
     (f o g)  o h = f  o (g  o h )
 
@@ -96,42 +107,42 @@
 
     a o id (domain a) = a = id (domain a)  o a
 
---A cateogy of data
+--A category of data
 
 A code generate an output type and it becomes an input type of next code. It is similar to a code is in between an input type and an output type.
 Is is possible to think data is an arrow between codes?
 
-<center><img src="fig/dataGear.jpg"></center>
+<center><img src="fig/dataGear.svg"></center>
 
-In other words, is there any duality in codes and data? Ususall answer is no, since we cannot simply combine data segments,
+In other words, is there any duality in codes and data? Usual answer is no, since we cannot simply combine data segments,
 but introducing continuation, it is possible to create a category which objects are functions and
 which arrows are data. Actually these two categories are dual in the sense of adjunction, that is
-there is a one to one corespondense between their arrows with isomorphism.
+there is a one to one correspondence between their arrows with isomorphism.
 Here we show the duality as an exercise of a category theory.
 
-The problem of data segments compisition is that it forgets about later computation. We can simply store it as a continuation in the
+The problem of data segments composition is that it forgets about later computation. We can simply store it as a continuation in the
 data segment. Data segments now have a continuation, which is a code segment. It is a part of meta computation. We have a data $f$, 
 which is a codomain of a code $a$ and is a domain of code $b$. A continuation of $f$ will called before the execution of code $b$.
 
-Now an data arrow $f$ is a triplet ${a,b,n}$, $a$ is a code which codomain is data $f$ and $b$ is a code wich domain is data $f$.
+Now an data arrow $f$ is a triplet ${a,b,n}$, $a$ is a code which codomain is data $f$ and $b$ is a code which domain is data $f$.
 $n : codomain a →  domain b $ is a continuation of $f$.
 
-We introdue access function as follows:
+We introduce access function as follows:
 
     data-domain f = a
     data-codomain   f = b
     continuation f = n
 
-We use data-codomain and data-comain for new Data Category C, which  is constructed from a category C. 
+We use data-codomain and data-codomain for new Data Category C, which  is constructed from a category C. 
 Objects of Data category C are arrows of category C. An arrow of Data category C from $a$ to $c$ is
-a data segment $f$ with continuation $n$,  $b'$ is a intermidiate data segment.
+a data segment $f$ with continuation $n$,  $b'$ is a intermediate data segment.
 
     n : codomain a  → domain b
     f = {a,b,n}
 
 $f$ is an arrow from $a$ to $b$.
 
-<center><img src="fig/dataGearComposition.jpg"></center>
+<center><img src="fig/dataGearComposition.svg"></center>
 
 If $f$ and $g$ has same data-domain and data-codomain, an equality of $f$ and $g$ is defined as follows,
 
@@ -139,7 +150,7 @@
 
 where $b$ is data-codomain of $f$ and $g$.
 
-Compisition of arrows of Data category is defined as follows.
+Composition of arrows of Data category is defined as follows.
 
     {b,c,m}  ∙ {a,b,n}  = {a,c,m o (b o n))}
 
@@ -155,13 +166,13 @@
 To make an identity arrow in the Data category, if $a$ is a codomain of $f$, we need a reverse arrow of $a$, $a'$.
 So every arrows $a$ in C have to have a reverse arrow $a'$, where
 
-    a  o a' =  id (codmain a)
+    a  o a' =  id (codomain a)
 
-Then an identity data segment  of $a$ in Data Categoy C is
+Then an identity data segment  of $a$ in Data Category C is
 
     {a,a,a'}
 
-<center><img src="fig/IdDataGear.jpg"></center>
+<center><img src="fig/IdDataGear.svg"></center>
 
 To check $data(f,a')$ is an identity,
 
@@ -172,14 +183,14 @@
 
 --A trivial duality of code and data
 
-<center><img src="fig/Duality.jpg"></center>
+<center><img src="fig/Duality.svg"></center>
 
 
-Data category is a data segment with continuation, which is one step behind, so there is a trivial one to one corespondence. 
-It is also easy to show C and Data category C  is an adjuntion pair. We show it using a universal mapping problem.
+Data category is a data segment with continuation, which is one step behind, so there is a trivial one to one correspondence. 
+It is also easy to show C and Data category C  is an adjunction pair. We show it using a universal mapping problem.
 
 Data segments in a Data category C is an object of original category C, so it has an identity arrow,
-which is an object of Data Category C . Acturally, we have a map F,
+which is an object of Data Category C . Actually, we have a map F,
 
     F : Obj C → Obj (Data Category C)
     F a =  id a
@@ -189,10 +200,10 @@
     U d = codomain d
     U {a,b,n}  =  b o n
 
-wehre $d$ is an object of Data Category C, and ${a,b,n}$ is an arrow from $a$ to $b$, with continuation $n$.
-Identity law and distribution law of $U$ is easily checked as
+where $d$ is an object of Data Category C, and ${a,b,n}$ is an arrow from $a$ to $b$, with continuation $n$.
+Identity law and distribution law of $U$ is easyly checked as
 
-    U {a,a,a'}  =  a o a' = id (codmain a)
+    U {a,a,a'}  =  a o a' = id (codomain a)
 
 We need a mapping $η$, which will be a natural transformation. 
 
@@ -211,7 +222,7 @@
 
     U ( *f )  o (η a) =  (b  o (b'  o f) )  o id a = f
 
-is directry checke and $*f$ is unique, that is 
+is directly checked and $*f$ is unique, that is 
 
     if there is an arrow g $U g  o (η a) = f$ then $g = *f$.
 
@@ -227,28 +238,29 @@
 
 --Comparison
 
-Meta compuation in Haskell\cite{} is defined as set of explict monads. In Gears, meta computation is unique among the system,
+Meta computation in Haskell is defined as set of explicit monads. In Gears, meta computation is unique among the system,
 which is something like operating system kernel or libraries.
 
-In Open CL\cite{} or Cuda\cite{}, there is a code segment which is called kernel. The kernel runs parallelly in a GPU. The kernel
+In OpenCL\cite{opencl} or Cuda\cite{cuda}, there is a code segment which is called kernel. The kernel runs parallelly in a GPU. The kernel
 is very similar to our code segment.
 
-Object oriented languages, such as Smalltalk-80 or Java , has meta compuation as a virtual machines. It is very different from
-monad or meta computation of our Gears system. Data segment has no idenity such as Smalltalk's self, it can be copied easily,
-which is a very good property in a parallel compuation environment.
+Object oriented languages, such as Smalltalk-80 or Java , has meta computation as a virtual machines. It is very different from
+monad or meta computation of our Gears system. Data segment has no identity such as Smalltalk's self, it can be copied easyly,
+which is a very good property in a parallel computation environment.
 
-Code segment can be seen as a kind of Typed assembly language, which has typed input and predictable behaviour.
+Code segment can be seen as a kind of Typed assembly language, which has typed input and predictable behavior.
 
 In old age, there is a software design method called data flow diagram. Category of code and data is very much like
-data flow diagram approach. It can be seen as a rivival of main frame technologies.
+data flow diagram approach. It can be seen as a revival of main frame technologies.
 
 
 --Conclusion
 
-As usual categorrical result, trivial duality of category and Data category means nothing itself.
+As usual categorical result, trivial duality of category and Data category means nothing itself.
 During the design of gears system, we see similarities of code segment and data segment. It has
-meta segments and contnuations. We think the duality gives us some guidance to design software
+meta segments and continuations. We think the duality gives us some guidance to design software
 system such as an operating system or libraries.
 
-We have implemented Gears system on top of LLVM\cite{} and hope it can be used as real sysetm description language.
+We have implemented Gears system on top of LLVM\cite{LLVM} and hope it can be used as real system description language.
 
+

--- a/lola2015.tex	Tue May 12 04:07:34 2015 +0900
+++ b/lola2015.tex	Tue May 12 10:44:14 2015 +0900
@@ -1,34 +1,98 @@
-\documentclass[envcountsame]{llncs}
+\documentclass[conference]{IEEEtran}
 \usepackage[dvipdfmx]{graphicx}
-\usepackage{llncsdoc}
+\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={@},
+}
 
-\bibliographystyle{plain} % for bibliography
-%\title{The implementation of recursive type syntax on GCC-4.6 for CbC}
-\title{Recursive type syntax in Continuation based C}
-\titlerunning{title running}
-\toctitle{toc title}
-%\subtitle{sub title}
-\author{Shinji Kono\inst{1} Nobuyasu Oshiro\inst{2}}
-\authorrunning{authorrunning}
-\institute{University of the Ryukyus}
-\email{}
+\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}
-\maketitle
-\input common
+%
+% 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{ Programming in code and data and its duality}
+
 
+% author names and affiliations
+% use a multiple column layout for up to three different
+% affiliations
+\author{
+\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
+% As a general rule, do not put math, special symbols or citations
+% in the abstract
 \begin{abstract}
-\input{abstract}
+\input{abstract}	
 \end{abstract}
 
-%\pagenumbering{arabic}
+% 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
 
 \input{0}	% sections
 
 \bibliography{ref}
-\nocite{r4rs,CompilingWithContinuation,kono08f}
-
 \end{document}