@article{oai:soar-ir.repo.nii.ac.jp:00018391, author = {Okazaki, Hiroyuki and Futa, Yuichi and Shidama, Yasunari}, issue = {2}, journal = {Formalized Mathematics}, month = {Jun}, note = {Article, Formalized Mathematics. 21(2): 133-143 (2013)}, pages = {133--143}, title = {Constructing Binary Huffman Tree}, volume = {21}, year = {2013} }