@article{Stallings1983,
 author = {John R. Stallings},
 title = {Topology of finite graphs},
 journal = {Inventiones Mathematicae},
 volume = {71},
 number = {3},
 year = {1983},
 pages = {551--565},
 doi = {10.1007/BF02095993},
 note = {DOI: \url{https://doi.org/10.1007/BF02095993}}
}
@article{KapovichMyasnikov2002,
 author = {Ilya Kapovich and Alexei Myasnikov},
 title = {Stallings foldings and subgroups of free groups},
 journal = {Journal of Algebra},
 volume = {248},
 number = {2},
 year = {2002},
 pages = {608--668},
 doi = {10.1006/jabr.2001.9033},
 note = {DOI: \url{https://doi.org/10.1006/jabr.2001.9033}. Preprint titled \emph{Stallings foldings and the subgroup structure of free groups}, arXiv:math/0202285}
}
@misc{StallingsArtifact,
 author = {Arthur Freitas Ramos},
 title = {Verified finite automata for finitely generated subgroups of {$F_2$}},
 year = {2026},
 howpublished = {\url{https://github.com/Arthur742Ramos/stallings-folding/tree/117dde0a8415d3da1787e15ad22a6223a744432d}},
 note = {Immutable source commit 117dde0a8415d3da1787e15ad22a6223a744432d; accessed October 1, 2026}
}
@misc{MathlibPinned,
 author = {{The Mathlib Community}},
 title = {Mathlib free-group reduction library},
 year = {2026},
 howpublished = {\url{https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/GroupTheory/FreeGroup/Reduce.lean}},
 note = {Pinned commit db584cd6d46c92f209a44c0f1c829460d327499d; accessed October 1, 2026}
}
@misc{PalomarRecord,
 author = {{Palomar Registry}},
 title = {Verified finite automata for finitely generated subgroups of {$F_2$}},
 year = {2026},
 howpublished = {\url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-23-000004\&version=1}},
 note = {PALOMAR-2026-09-23-000004, version 1; registered September 23, 2026; accessed October 1, 2026}
}