\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の実装}}{4}{}\protected@file@percent }
\newlabel{agda-dpp-state}{{5}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}{\ignorespaces Gears Agdaでの DPP の 哲学者の状態}}{4}{}\protected@file@percent }
\newlabel{agda-dpp-process}{{6}{4}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}{\ignorespaces Gears Agdaでの DPP の プロセス}}{4}{}\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{agda-alpa}{2}
\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{5}{}\protected@file@percent }
\newlabel{agda-dpp-bruteforce}{{11}{5}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の場合を網羅するコード}}{5}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent }
\bibcite{ats2}{3}
\bibcite{cbc-gcc}{4}
\bibcite{cbc-llvm}{5}
\bibcite{coq}{6}
\bibcite{agda-alpa-old}{7}
\bibcite{agda2-hoare}{8}
\bibcite{loop-proof}{9}
\bibcite{rust}{10}
\bibcite{coq-old}{11}
\bibcite{agda-documentation}{12}
\bibcite{cr-ryukyu}{13}
\bibcite{10.1145/363235.363259}{14}
\bibcite{kaito-lola}{15}
\bibcite{Klein:2010:SFV:1743546.1743574}{16}
\bibcite{moggi-monad}{17}
\bibcite{Nelson:2017:HPV:3132747.3132748}{18}
\bibcite{agda}{19}
\bibcite{Stump:2016:VFP:2841316}{20}
\bibcite{parusu-master}{21}
\bibcite{ryokka-sigos}{22}
\bibcite{mitsuki-master}{23}
\bibcite{mitsuki-prosym}{24}
\bibcite{atton-ipsj}{25}
\bibcite{weko_82695_1}{26}
\bibcite{utah-master}{27}
\bibcite{atton-master}{28}
\newlabel{ipsj@lastpage}{{}{6}}
\gdef \@abspage@last{6}