Infinite Words and Morphic Languages Formalized in Isabelle/HOL
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). First posted on arXiv 20 Mar 2023.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2026: 1.
1 paper.
- 2026LAMP: Lean-based Agentic framework with MCP and Proof Repair27 Jun 2026