Cotoleta –Lean Library for Formalized Coding Theory–

Last Update: 2021/Sep./22

This is the official website of cotoleta.
Cotoleta is a LEAN library for formalized coding theory
and stands for COding Theory Over the LEan Theorem-proof Assistant.

Formalized Objects:
-Repetition Codes
-Hamming Codes
-Levenshtein Distances, Edit Distance, Insertion/Deletion Codes

Our library is available from the link below:
-lean 2: -= Cotoleta version 0.11 beta =-(2016/Sep./30)

-lean 3.3: -= CotoletaInsDel version 0.1 beta =-(2018/April/28)

-lean 3.4.1: -= CotoletaInsDel version 0.1 beta =-(2018/Oct/26)

-lean 3.4.2: -= CotoletaLevCodes version 0.1 beta =-(2019/Nov./7)

-lean 3.4.2: -=CotoletaVTCodes version 0.1 beta=-(2020/Apr./22)
-lean 3.4.2: -=CotoletaVTCodes version 0.1 beta=-(2021/Feb./08)
-lean 3.4.2: -=CotoletaVTCodes version 0.2 beta=-(2021/Sep./22)

-Formalization of Coding Theory using Lean,
Manabu Hagiwara, Kyosuke Nakano and Justin Kong,
ISITA2016, California, 2016.

Formalized by
-Manabu Hagiwara
-Justin Kong
-Kyosuke Nakano
-Devid Webb
-Yuki Kondou

Since 2016.