\relax 
\@writefile{toc}{\contentsline {section}{\numberline {1}ソフトウェアの信頼性の保証}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {2}Countinuation based C (CbC)}{1}}
\newlabel{src:goto}{{1}{1}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCコードの例}{1}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces ソースコード1\relax の流れ}}{1}}
\newlabel{fig:code_simple}{{1}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {3}CbC における Interface の定義}{1}}
\citation{agda}
\newlabel{src:interface}{{2}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}CbCでのStack-Interfaceの実装}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Agda}{2}}
\newlabel{src:agda-css}{{3}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {3}Agda における CodeSegment の定義}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Agda における Interface の定義、実装}{2}}
\newlabel{src:agda-interface}{{4}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {4}Agda における Stack -Interface の定義の一部}{2}}
\newlabel{src:agda-single-linked-stack}{{5}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {5}Agda における Stack -Interface の実装の一部}{2}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Agda による Interface 部分を含めた Stack の部分的な証明}{2}}
\newlabel{src:agda-in-some-state}{{6}{2}}
\@writefile{lol}{\contentsline {lstlisting}{\numberline {6}抽象的なStackの定義とpush$->$push$->$pop2 の証明}{2}}
\citation{*}
\bibstyle{junsrt}
\bibdata{reference}
\bibcite{agda}{1}
\bibcite{Yasutaka:2016}{2}
\bibcite{Tatsuki:2016}{3}
\bibcite{kaito:2015}{4}
\bibcite{agda-documentation}{5}
\@writefile{toc}{\contentsline {section}{\numberline {7}まとめ}{3}}