Mercurial > hg > Papers > 2015 > atton-thesis
changeset 54:bf136bd59e7a
Add thebibliography
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 16 Feb 2015 12:40:53 +0900 |
| parents | ca389989b660 |
| children | 43213dcf8d24 |
| files | .hgignore Makefile agda.tex bibliography.tex category.tex functional_programming.tex introduction.tex main.tex reference.bib |
| diffstat | 9 files changed, 75 insertions(+), 31 deletions(-) [+] |
line wrap: on
line diff
--- a/.hgignore Sun Feb 15 22:38:43 2015 +0900 +++ b/.hgignore Mon Feb 16 12:40:53 2015 +0900 @@ -5,6 +5,8 @@ *.swp *.*~ +*.bbl +*.blg *.lof *.lol *.lot
--- a/Makefile Sun Feb 15 22:38:43 2015 +0900 +++ b/Makefile Mon Feb 16 12:40:53 2015 +0900 @@ -7,16 +7,17 @@ $(TARGET).dvi : $(wildcard *.tex) $(wildcard fig/*.pdf) ruby replace_agda.rb - platex $(TARGET).tex - platex $(TARGET).tex - platex $(TARGET).tex + platex $(TARGET).tex + pbibtex $(TARGET) + platex $(TARGET).tex + platex $(TARGET).tex # commands .PHONY : clean all open remake setup clean: - rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol + rm -f *.dvi *.aux *.log *.pdf *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg all: $(TARGET).pdf
--- a/agda.tex Sun Feb 15 22:38:43 2015 +0900 +++ b/agda.tex Mon Feb 16 12:40:53 2015 +0900 @@ -15,7 +15,7 @@ \section{Natural Deduction} \label{section:natural_deduction} 証明には natural deduction(自然演繹)を用いる。 -natural deduction は Gentzen によって作られた論理と、その証明システムである。 +natural deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。 命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。 natural deduction において
--- a/bibliography.tex Sun Feb 15 22:38:43 2015 +0900 +++ b/bibliography.tex Mon Feb 16 12:40:53 2015 +0900 @@ -1,25 +1,5 @@ % 参考文献 \def\line{−\hspace*{-.7zw}−} -\begin{thebibliography}{99} -%\bibitem{*}内の * は各自わかりやすい名前などをつけて、 -%論文中には \cite{*} のように使用する。 -%これをベースに書き換えた方が楽かも。 -%書籍、論文、URLによって若干書き方が異なる。 -%URLを載せる人は参考にした年月日を最後に記入すること。 - -% TODO: List - -% books -% proofs and types -% Introduction to higher order categorical logic -% category theory for the computiong science - -% papers -% notion of computations and monads -% composing monads - - -\bibitem{hoge} -hoge -\end{thebibliography} +\bibliographystyle{jplain} +\bibliography{reference}
--- a/category.tex Sun Feb 15 22:38:43 2015 +0900 +++ b/category.tex Mon Feb 16 12:40:53 2015 +0900 @@ -3,7 +3,7 @@ \ref{chapter:delta}章ではプログラムの変更がメタ計算としてMonadを用いて定義可能であることを示した。 \ref{chapter:category}章では category により Monad の定義と要請されるMonad則について述べる。 -定義は Monad の解説に必要な部分についてのみ解説する。 +定義は Monad の解説に必要な部分についてのみ解説する~\cite{opac-b1092711}~\cite{BarrM:cattcs}。 % {{{ Category
--- a/functional_programming.tex Sun Feb 15 22:38:43 2015 +0900 +++ b/functional_programming.tex Mon Feb 16 12:40:53 2015 +0900 @@ -152,7 +152,7 @@ functor の定義にあたり、\ref{section:functor}節で示したように Functor則を満たすようにデータ型と fmap を定義しなくてはならない。 -Haskell における Functor則はリスト\ref{src:functor_laws_in_haskell}のように表される。 +Haskell における Functor則はリスト\ref{src:functor_laws_in_haskell}のように表される~\cite{JonesDuponcheel93}。 \begin{table}[html] \lstinputlisting[label=src:functor_laws_in_haskell, caption=Haskellにおける Functor則] {src/functor_laws_in_haskell.txt}
--- a/introduction.tex Sun Feb 15 22:38:43 2015 +0900 +++ b/introduction.tex Mon Feb 16 12:40:53 2015 +0900 @@ -9,7 +9,7 @@ よって、プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。 本研究ではプログラムの変更を Monad を用いて形式化する。 -プログラムにおけるMonad とはデータ構造とメタ計算の対応である。 +プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。 メタ計算とは計算を実現するための計算であり、プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行することができる。 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を考える。 もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと判定できる。
--- a/main.tex Sun Feb 15 22:38:43 2015 +0900 +++ b/main.tex Mon Feb 16 12:40:53 2015 +0900 @@ -3,7 +3,7 @@ \usepackage{mythesis} \usepackage{multirow} \usepackage{here} -\usepackage{float} +\usepackage{cite} \usepackage{listings} \usepackage{bussproofs} \usepackage{amssymb}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/reference.bib Mon Feb 16 12:40:53 2015 +0900 @@ -0,0 +1,61 @@ +@book{Girard:1989:PT:64805, + author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves}, + title = {Proofs and Types}, + year = {1989}, + isbn = {0-521-37181-3}, + publisher = {Cambridge University Press}, + address = {New York, NY, USA}, +} + +@book{opac-b1092711, + title = "Introduction to higher order categorical logic", + author = "Lambek, Joachim (mathématicien) and Scott, P. J.", + series = "Cambridge studies in advanced mathematics", + publisher = "Cambridge University Press", + address = "Cambridge, New York (N. Y.), Melbourne", + url = "http://opac.inria.fr/record=b1092711", + isbn = "0-521-24665-2", + year = 1986 +} + +@book{BarrM:cattcs, + author = {Barr, Michael and Wells, Charles}, + title = {Category Theory for Computing Science}, + publisher = {Prentice-Hall}, + series = {International Series in Computer Science}, + year = 1990, + note = {Second edition, 1995}, + isbn = {0-13-120486-6}, + lccn = {QA76.9.M35B37 1990} +} + +@article{Moggi:1991:NCM:116981.116984, + author = {Moggi, Eugenio}, + title = {Notions of Computation and Monads}, + journal = {Inf. Comput.}, + issue_date = {July 1991}, + volume = {93}, + number = {1}, + month = jul, + year = {1991}, + issn = {0890-5401}, + pages = {55--92}, + numpages = {38}, + url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4}, + doi = {10.1016/0890-5401(91)90052-4}, + acmid = {116984}, + publisher = {Academic Press, Inc.}, + address = {Duluth, MN, USA}, +} + +@techreport{JonesDuponcheel93, + author = {M. P. Jones and L. Duponcheel}, + title = {Composing monads}, + institution = {Yale University}, + year = {1993}, + month = {December}, + number = {YALEU/DCS/RR-1004}, + type = {Research Report}, + ftp = {ftp://ftp.cs.nott.ac.uk/nott-fp/reports/yale/RR-1004.ps} +} +