Mercurial > hg > Papers > 2020 > soto-midterm
annotate tex/agda.tex @ 4:35f0e5f12fe6
add verification method
| author | soto@cr.ie.u-ryukyu.ac.jp |
|---|---|
| date | Fri, 11 Sep 2020 02:30:15 +0900 |
| parents | b124f02ea3f1 |
| children | 4bf00f7ba825 |
| rev | line source |
|---|---|
| 4 | 1 \section{Agda} |
| 2 Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ | |
| 3 ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは | |
| 4 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で | |
| 5 は記述したプログラムを証明することができる。 | |
| 6 | |
| 7 %\subsection{Record 型} | |
| 8 | |
| 9 %\subsection{Data 型} | |
| 10 | |
| 11 %\subsection{Agdaの基本操作} | |
| 12 | |
| 13 %\subsection{定理証明支援器としての Agda} | |
| 14 | |
| 15 %\subsectoin{} | |
| 16 | |
| 17 |