@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}
}