Infinite Words and Morphic Languages Formalized in Isabelle/HOL
Formal Languages and Automata Theory
2023-03-22 v1 Logic in Computer Science
Abstract
We present a formalization of basics related to infinite words in the generic proof assistant Isabelle/HOL. Furthermore, we present a formalization of purely morphic and morphic languages. Finally, we present a formalized definition of Sturmian words as lower mechanical words and prove some very elementary facts. The formalization is based on an ongoing larger project of formalization of combinatorics on words.
Cite
@article{arxiv.2303.11445,
title = {Infinite Words and Morphic Languages Formalized in Isabelle/HOL},
author = {Štěpán Starosta},
journal= {arXiv preprint arXiv:2303.11445},
year = {2023}
}
Comments
Submitted to Words 2023