Mercurial > hg > Papers > 2020 > soto-midterm
comparison 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 |
comparison
equal
deleted
inserted
replaced
3:b124f02ea3f1 | 4:35f0e5f12fe6 |
---|---|
1 \section{agda} | 1 \section{Agda} |
2 agdaとは、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 |