\documentclass[a4j,12pt]{jreport}
\usepackage{master_paper}
\usepackage{ascmac}
\usepackage[dvipdfmx]{graphicx}
\usepackage{here}
\usepackage{listings}
\usepackage{comment}
\usepackage[deluxe, multi]{otf}
\usepackage{url}
\usepackage{cite}
\usepackage{listings}
\usepackage{bussproofs}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage[utf8]{inputenc}

%\input{dummy.tex} %% font

\jtitle{メタ計算を用いた Continuation based C の検証手法}
\etitle{Verification Methods of Continuation based C using Meta Computations}
\year{2017年 3月}
\eyear{March 2017}
\author{比嘉 健太}
\eauthor{Yasutaka HIGA}
\chife{指導教員：教授　和田 知久}
\echife{Supervisor: Prof. Tomohisa WADA}

\marklefthead{% 左上に挿入
  \begin{minipage}[b]{.4\textwidth}
    琉球大学大学院学位論文(修士)
\end{minipage}}

\markleftfoot{% 左下に挿入
  \begin{minipage}{.8\textwidth}
    メタ計算を用いた Continuation based C の検証手法
\end{minipage}}

\newcommand\figref[1]{図 \ref{fig:#1}}
\newcommand\tabref[1]{表 \ref{tab:#1}}

\lstset{
  frame=single,
  keepspaces=true,
  stringstyle={\ttfamily},
  commentstyle={\ttfamily},
  identifierstyle={\ttfamily},
  keywordstyle={\ttfamily},
  basicstyle={\ttfamily},
  breaklines=true,
  xleftmargin=0zw,
  xrightmargin=0zw,
  framerule=.2pt,
  columns=[l]{fullflexible},
  numbers=left,
  stepnumber=1,
  numberstyle={\scriptsize},
  numbersep=1em,
  language={},
  tabsize=4,
  lineskip=-0.5zw,
  escapechar={@},
}
\def\lstlistingname{リスト}
\def\lstlistlistingname{リスト目次}

%%% 索引のために以下の2行を追加
\usepackage{makeidx,multicol}
\makeindex
\begin{document}

%rome
\frontmatter

\maketitle
\newpage

\makecommission

%要旨
\input{abstract.tex}
\input{abstract_eng.tex}

%目次
\tableofcontents

%図目次
\listoffigures

%表目次
\listoftables

%リスト目次
\lstlistoflistings


%arabic
\mainmatter

%chapters
\input{introduction.tex}

\input{cbc.tex}

\chapter{ラムダ計算と型システム}
\label{chapter:type}
\section{型システムとは}
\section{型なしラムダ計算}
\section{単純型付きラムダ計算}
\section{部分型付け}
\section{部分型と Continuation based C}

\chapter{証明支援系言語 Agda による証明手法}
\label{chapter:agda}
\section{依存型を持つ証明支援系言語 Agda}
\section{Natural Deduction}
\section{Curry-Howard Isomorphism}
\section{Reasoning}

\chapter{Agda における Continuation based C の表現}
\label{chapter:subtype}
\section{CodeSegment の定義}
\section{DataSegment の定義}
\section{ノーマルレベル計算の実行}
\section{MetaCodeSegment の定義}
\section{MetaDataSegment の定義}
\section{メタレベル計算の実行}
\section{Agda を用いたContinuation based C の検証}
\section{スタックの実装の検証}

\chapter{まとめ}
\section{今後の課題}

%謝辞
\addcontentsline{toc}{chapter}{謝辞}
\input{thanks.tex}

%参考文献
\nocite{*}
\bibliographystyle{junsrt}
\bibliography{reference}

%発表履歴
\addcontentsline{toc}{chapter}{発表履歴}
\input{history.tex}

%付録
\addcontentsline{toc}{chapter}{付録}
% \input{appendix.tex}
\end{document}