@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00232294, author = {河野, 真治 and Shinji, KONO}, book = {第64回プログラミング・シンポジウム予稿集}, month = {Jan}, note = {集合論は数学では古典的な基礎なので避けて通れない。Agda は Curry Howward 対応で証明を記述できる純関数型言語である。Agda 向きの集合論の公理を提案し、その有用性示すの例題として Zorn の補題の証明を行った。Zorn の補題はチコノフの定理などに使われる重要な定理であり、それを証明付きデータ構造を用いてAgdaで証明する。直観主義論理での集合論について考察する。}, pages = {5--16}, publisher = {情報処理学会}, title = {Agda による Zorn の補題の証明}, volume = {2023}, year = {2023} }