WEKO3
アイテム
Agda によるガロア理論
https://ipsj.ixsq.nii.ac.jp/records/232243
https://ipsj.ixsq.nii.ac.jp/records/232243e68fd914-74a5-4614-95de-481af5273c9a
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-WPRO2021005.pdf (486.7 kB)
|
Copyright (c) 2021 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2021-01-08 | |||||||
| タイトル | ||||||||
| タイトル | Agda によるガロア理論 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Galois Theory in Agda | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | Agda, Galois, Proof | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| 琉球大学工学部 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Faculty of Engineering, University of the Ryukyus | ||||||||
| 著者名 |
河野, 真治
× 河野, 真治
|
|||||||
| 著者名(英) |
Shinji, KONO
× Shinji, KONO
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | Agda は省略可能な型変数を持つ純関数型言語であり、カーリーハワード対応に基づく証明支援系として使うことができる。数学的な命題は型として記述され、その証明は型を実現するλ項として記述される。ここではガロア理論の対称群の可解性について証明を行ない、証明付きのデータ構造の有効性を確認した。 | |||||||
| 書誌情報 |
第62回プログラミング・シンポジウム予稿集 巻 2021, p. 25-33, 発行日 2021-01-08 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
