2026-03-14T13:44:04Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00232243 2025-01-19T10:30:33Z 6164:6805:6807:11587

Agda によるガロア理論 Galois Theory in Agda 河野, 真治 Shinji, KONO Agda, Galois, Proof Agda は省略可能な型変数を持つ純関数型言語であり、カーリーハワード対応に基づく証明支援系として使うことができる。数学的な命題は型として記述され、その証明は型を実現するλ項として記述される。ここではガロア理論の対称群の可解性について証明を行ない、証明付きのデータ構造の有効性を確認した。 conference paper 情報処理学会 2021-01-08 application/pdf 第62回プログラミング・シンポジウム予稿集 2021 25 33 https://ipsj.ixsq.nii.ac.jp/record/232243/files/IPSJ-WPRO2021005.pdf jpn