\relax 
\citation{kaito-lola}
\newlabel{ipsj@firstpage}{{}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}\hskip 1zw{Gears Agda でのモデル検査}}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {2}\hskip 1zw{Continuation based C}}{1}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces メタ計算を可視化した CodeGear と DataGear\relax }}{2}{}\protected@file@percent }
\providecommand*\caption@xref[2]{\@setref\relax\@undefined{#1}}
\newlabel{fig:meta-cgdg}{{1}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {3}\hskip 1zw{GearsAgda 形式で書く Agda}}{2}{}\protected@file@percent }
\newlabel{agda-dg}{{1}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}{\ignorespaces Agdaでの Data Gear の定義}}{2}{}\protected@file@percent }
\newlabel{agda-cg}{{2}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}{\ignorespaces Agdaでの Code Gear の定義}}{2}{}\protected@file@percent }
\newlabel{agda-not-cg}{{3}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}{\ignorespaces Agdaでの 停止性が示せない CodeGear の例}}{2}{}\protected@file@percent }
\newlabel{agda-exec-cg}{{4}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}{\ignorespaces Agdaでの CodeGear の初期化}}{2}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}{Agda による Meta Gears}}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {4}\hskip 1zw{モデル検査}}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {5}\hskip 1zw{Dining Philosophers Problem}}{3}{}\protected@file@percent }
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces メタ計算を可視化した CodeGear と DataGear\relax }}{3}{}\protected@file@percent }
\newlabel{fig:DPP}{{2}{3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}{Gears Agda によるDPPの実装}}{3}{}\protected@file@percent }
\newlabel{agda-dpp-state}{{5}{3}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}{\ignorespaces Gears Agdaでの DPP の 哲学者の状態}}{3}{}\protected@file@percent }
\newlabel{agda-dpp-process}{{6}{3}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}{\ignorespaces Gears Agdaでの DPP の プロセス}}{3}{}\protected@file@percent }
\newlabel{agda-dpp-dg}{{7}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {7}{\ignorespaces Gears Agdaでの DPP の Data Gear}}{4}{}\protected@file@percent }
\newlabel{agda-dpp-init}{{8}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {8}{\ignorespaces Gears Agdaでの DPP の Data Gear のinit}}{4}{}\protected@file@percent }
\newlabel{agda-dpp-step}{{9}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {9}{\ignorespaces Gears Agdaでの DPP の step 実行}}{4}{}\protected@file@percent }
\newlabel{agda-dpp-lfork}{{10}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {10}{\ignorespaces Gears Agdaでの DPP の左のフォークを取る記述}}{4}{}\protected@file@percent }
\citation{*}
\bibstyle{ipsjsort}
\bibdata{reference}
\bibcite{agda-wiki}{1}
\bibcite{kaito-lola}{2}
\bibcite{Stump:2016:VFP:2841316}{3}
\bibcite{parusu-master}{4}
\bibcite{ryokka-sigos}{5}
\bibcite{atton-ipsj}{6}
\bibcite{utah-master}{7}
\bibcite{atton-master}{8}
\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPP のモデル検査}}{5}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent }
\newlabel{ipsj@lastpage}{{}{5}}
\gdef\svg@ink@ver@settings{{\m@ne }{inkscape}{\m@ne }}
\gdef \@abspage@last{5}