Mercurial > hg > Papers > 2022 > soto-sigos

comparison Paper/soto-sigos.aux @ 3:952d4dbb7c6a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
WIP 仮完成
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 05 May 2022 03:30:26 +0900
parents f9794e92f964
children 7434c0aa1859
comparison
equal deleted inserted replaced
2:f9794e92f964 3:952d4dbb7c6a
16 \newlabel{agda-exec-cg}{{4}{2}} 16 \newlabel{agda-exec-cg}{{4}{2}}
17 \@writefile{lol}{\contentsline {lstlisting}{\numberline {4}{\ignorespaces Agdaでの CodeGear の初期化}}{2}{}\protected@file@percent } 17 \@writefile{lol}{\contentsline {lstlisting}{\numberline {4}{\ignorespaces Agdaでの CodeGear の初期化}}{2}{}\protected@file@percent }
18 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}{agda による Meta Gears}}{3}{}\protected@file@percent } 18 \@writefile{toc}{\contentsline {subsection}{\numberline {3.1}{agda による Meta Gears}}{3}{}\protected@file@percent }
19 \@writefile{toc}{\contentsline {section}{\numberline {4}\hskip 1zw{モデル検査}}{3}{}\protected@file@percent } 19 \@writefile{toc}{\contentsline {section}{\numberline {4}\hskip 1zw{モデル検査}}{3}{}\protected@file@percent }
20 \@writefile{toc}{\contentsline {section}{\numberline {5}\hskip 1zw{Dining Philosophers Problem}}{3}{}\protected@file@percent } 20 \@writefile{toc}{\contentsline {section}{\numberline {5}\hskip 1zw{Dining Philosophers Problem}}{3}{}\protected@file@percent }
21 \@writefile{toc}{\contentsline {subsection}{\numberline {5.1}{Gears Agda によるDPPの実装}}{3}{}\protected@file@percent } 21 \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces メタ計算を可視化した CodeGear と DataGear\relax }}{3}{}\protected@file@percent }
22 \newlabel{agda-dpp-state}{{5}{3}} 22 \newlabel{fig:DPP}{{2}{3}}
23 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5}{\ignorespaces Gears Agdaでの DPP の 哲学者の状態}}{3}{}\protected@file@percent } 23 \@writefile{toc}{\contentsline {subsection}{\numberline {5.1}{Gears Agda によるDPPの実装}}{4}{}\protected@file@percent }
24 \newlabel{agda-dpp-process}{{6}{3}} 24 \newlabel{agda-dpp-state}{{5}{4}}
25 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6}{\ignorespaces Gears Agdaでの DPP の プロセス}}{3}{}\protected@file@percent } 25 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5}{\ignorespaces Gears Agdaでの DPP の 哲学者の状態}}{4}{}\protected@file@percent }
26 \newlabel{agda-dpp-process}{{6}{4}}
27 \@writefile{lol}{\contentsline {lstlisting}{\numberline {6}{\ignorespaces Gears Agdaでの DPP の プロセス}}{4}{}\protected@file@percent }
26 \newlabel{agda-dpp-dg}{{7}{4}} 28 \newlabel{agda-dpp-dg}{{7}{4}}
27 \@writefile{lol}{\contentsline {lstlisting}{\numberline {7}{\ignorespaces Gears Agdaでの DPP の Data Gear}}{4}{}\protected@file@percent } 29 \@writefile{lol}{\contentsline {lstlisting}{\numberline {7}{\ignorespaces Gears Agdaでの DPP の Data Gear}}{4}{}\protected@file@percent }
28 \newlabel{agda-dpp-init}{{8}{4}} 30 \newlabel{agda-dpp-init}{{8}{4}}
29 \@writefile{lol}{\contentsline {lstlisting}{\numberline {8}{\ignorespaces Gears Agdaでの DPP の Data Gear のinit}}{4}{}\protected@file@percent } 31 \@writefile{lol}{\contentsline {lstlisting}{\numberline {8}{\ignorespaces Gears Agdaでの DPP の Data Gear のinit}}{4}{}\protected@file@percent }
30 \newlabel{agda-dpp-step}{{9}{4}} 32 \newlabel{agda-dpp-step}{{9}{4}}
31 \@writefile{lol}{\contentsline {lstlisting}{\numberline {9}{\ignorespaces Gears Agdaでの DPP の step 実行}}{4}{}\protected@file@percent } 33 \@writefile{lol}{\contentsline {lstlisting}{\numberline {9}{\ignorespaces Gears Agdaでの DPP の step 実行}}{4}{}\protected@file@percent }
32 \newlabel{agda-dpp-lfork}{{10}{4}} 34 \newlabel{agda-dpp-lfork}{{10}{4}}
33 \@writefile{lol}{\contentsline {lstlisting}{\numberline {10}{\ignorespaces Gears Agdaでの DPP の 左のフォークを取るコード}}{4}{}\protected@file@percent } 35 \@writefile{lol}{\contentsline {lstlisting}{\numberline {10}{\ignorespaces Gears Agdaでの DPP の左のフォークを取る記述}}{4}{}\protected@file@percent }
34 \@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{4}{}\protected@file@percent }
35 \citation{*} 36 \citation{*}
36 \bibstyle{ipsjsort} 37 \bibstyle{ipsjsort}
37 \bibdata{reference} 38 \bibdata{reference}
38 \bibcite{agda-wiki}{1} 39 \bibcite{agda-wiki}{1}
39 \bibcite{agda-alpa}{2} 40 \bibcite{agda-alpa}{2}
41 \@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{5}{}\protected@file@percent }
42 \newlabel{agda-dpp-bruteforce}{{11}{5}}
43 \@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の場合を網羅するコード}}{5}{}\protected@file@percent }
44 \@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent }
40 \bibcite{ats2}{3} 45 \bibcite{ats2}{3}
41 \bibcite{cbc-gcc}{4} 46 \bibcite{cbc-gcc}{4}
42 \bibcite{cbc-llvm}{5} 47 \bibcite{cbc-llvm}{5}
43 \bibcite{coq}{6} 48 \bibcite{coq}{6}
44 \bibcite{agda-alpa-old}{7} 49 \bibcite{agda-alpa-old}{7}
45 \bibcite{agda2-hoare}{8} 50 \bibcite{agda2-hoare}{8}
46 \bibcite{loop-proof}{9} 51 \bibcite{loop-proof}{9}
47 \bibcite{rust}{10} 52 \bibcite{rust}{10}
48 \bibcite{coq-old}{11} 53 \bibcite{coq-old}{11}
49 \bibcite{agda-documentation}{12} 54 \bibcite{agda-documentation}{12}
50 \newlabel{agda-dpp-bruteforce}{{11}{5}}
51 \@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の 左のフォークを取るコード}}{5}{}\protected@file@percent }
52 \@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent }
53 \bibcite{cr-ryukyu}{13} 55 \bibcite{cr-ryukyu}{13}
54 \bibcite{10.1145/363235.363259}{14} 56 \bibcite{10.1145/363235.363259}{14}
55 \bibcite{kaito-lola}{15} 57 \bibcite{kaito-lola}{15}
56 \bibcite{Klein:2010:SFV:1743546.1743574}{16} 58 \bibcite{Klein:2010:SFV:1743546.1743574}{16}
57 \bibcite{moggi-monad}{17} 59 \bibcite{moggi-monad}{17}