師玉康成(信州大学工学部情報工学科)
日本におけるMizarプロジェクトの現状と展望
発表スライド
岡崎裕之(信州大学大学院理工学系研究科)
Mizarの暗号理論への応用
資料
ハフマン符号の形式化Mizar版（随時更新中）
ボキャブラリーファイル
アーティクル本体