論文タイトル：  AgdaによるGalois理論のプログラミング

論文タイトル英語： Programming Galois Theory in Agda

キーワード： Agda Galois Proof

著者名： 河野真治

著者名英語：Shinji KONO

著者所属： 琉球大学工学部

著者所属英語： Faculty of Engineering, University of the Ryukyus

論文抄録（日本語論文の場合）：

Agda は省略可能な型変数を持つ純関数型言語であり、カーリーハワード対応に基づく証明支援系として使うことができる。
数学的な命題は型として記述され、その証明は型を実現するλ項として記述される。
ここではガロア理論の対称群の可解性について証明を行ない、証明付きのデータ構造の有効性を確認した。


論文抄録英語（英語論文の場合）：

Agda is pure functional language with implicit type variables, which can be used as a proof assistant system.
Mathematical concepts are described as types and proofs are described as lambda terms.
In this paper, we show the solvablity of symmetric group in Galois Theory. Effectiveness of Data structure with Proof is
demonstrated.