Summary
The 2018 International Symposium on Information Theory and Its Applications　(ISITA2018)
2018
Session Number:Mo-AM-1-1
Session:
Number:Mo-AM-1-1.3
Formalization of Insertion/Deletion Codes and the Levenshtein Metric in Lean
Justin Kong, David J. Webb, Manabu Hagiwara,
pp.11-15
Publication Date:2018/10/18
Online ISSN:2188-5079
DOI:10.34385/proc.55.Mo-AM-1-1.3
PDF download
Summary:
Formalization deals with expressing definitions or theorems and proofs at the level of fundamental logic, which allows for automatic verification by computer programs. We report on work done formalizing definitions and theorems in coding theory using the Lean theorem prover, released by Microsoft Research and Carnegie Mellon University in 2015. We formalize fundamental concepts regarding error-correcting codes capable of correcting insertions, deletions, or combinations of insertions and deletions. In particular, we formalize definitions and theorems about subsequences and supersequences, the Levenshtein distance, insertion/deletion spheres, and insertion/deletion codes.