# HG changeset patch # User ryokka # Date 1508997850 -32400 # Node ID 3be2444dacc59640df14bc39038110a553d3fb8a # Parent 8f91a416343dca4d712d6c1e825121dc568e0bd1 fix invisible header diff -r 8f91a416343d -r 3be2444dacc5 midterm/midterm.pdf Binary file midterm/midterm.pdf has changed diff -r 8f91a416343d -r 3be2444dacc5 midterm/midterm.tex --- a/midterm/midterm.tex Thu Oct 26 14:35:55 2017 +0900 +++ b/midterm/midterm.tex Thu Oct 26 15:04:10 2017 +0900 @@ -1,17 +1,12 @@ -%% TODO Agdaに関してやったこと書く -%% TODO AgdaのStackとcbcのstackを例として出す。 -%% TODO 自然演繹の推論規則を表にまとめて乗っける - - \documentclass[twocolumn,twoside,9.5pt]{jarticle} \usepackage[dvipdfmx]{graphicx} \usepackage{picins} -\usepackage{listings,jlisting} \usepackage{fancyhdr} +%\pagestyle{fancy} %\usepackage{abstract} -%\pagestyle{fancy} \usepackage{url} \usepackage{bussproofs} +\usepackage{listings,jlisting} \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿} \rhead{} \cfoot{} @@ -26,18 +21,9 @@ \setlength{\footskip}{0mm} \pagestyle{empty} -%% \lstset{% -%% breaklines=true -%% } - \lstset{ frame=single, keepspaces=true, - stringstyle={\ttfamily}, - commentstyle={\ttfamily}, - identifierstyle={\ttfamily}, - keywordstyle={\ttfamily}, - basicstyle={\ttfamily}, breaklines=true, xleftmargin=0zw, xrightmargin=0zw, @@ -51,15 +37,13 @@ \input{dummy.tex} -\renewcommand{\abstractname}{Abstract} +%\renewcommand{\abstractname}{Abstract} \begin{document} - \title{CbC言語によるプログラムの検証} - \author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治} \date{} - \maketitle +\thispagestyle{fancy} \section{研究目的} @@ -310,12 +294,11 @@ %% \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced} - \section{今後の課題} 現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。 今後は CbC での RedBlackTree の Deletion 、Agda での証明を実装していく。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題があるため、今後はこれらの課題に着手していく。 -\nocite{*} +%\nocite{*} \bibliographystyle{junsrt} \bibliography{reference} \end{document}