{"id":"palomar/PALOMAR-2026-08-27-000011","url":"https://github.com/nielstron/langlib/tree/10fb20454652d4b7f0f1710880f79240986021c6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000011-v2.json","repo":"https://github.com/nielstron/langlib","tags":["cs.FL","msc:68Q42","msc:68Q45","msc:68Q04","formal-languages","lean","chomsky-hierarchy","automata"],"score":0,"title":"nielstron/langlib","trust":"high","domain":"cs.FL","source":"palomar","authors":["Niels Mündler","Martin Dvořák"],"reviews":0,"subject":"cs.FL","summary":"A Lean 4 formalization of grammar and automaton presentations of the extended Chomsky hierarchy. Starting from unrestricted-grammar rewriting, it defines regular, linear, context-free, context-sensitive, indexed, deterministic context-free, recursive, and recursively enumerable language classes; relates finite, pushdown, linearly bounded, and Mathlib TM0 automata to the corresponding grammar classes; proves strict hierarchy inclusions; and establishes closure or non-closure under thirteen operations for seven major classes.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"Introduction to Automata Theory, Languages, and Computation, 3rd edition","identifier":"ISBN 978-0321455369","relationship":"formalizes"},{"title":"Indexed Grammars—An Extension of Context-Free Grammars","identifier":"doi:10.1145/321479.321488","relationship":"formalizes"},{"title":"Classes of Languages and Linear-Bounded Automata","identifier":"doi:10.1016/S0019-9958(64)90120-2","relationship":"formalizes"},{"title":"Linear Bounded Automata","identifier":"WADD Technical Note 60-165","relationship":"formalizes"},{"title":"On the Translation of Languages from Left to Right","identifier":"doi:10.1016/S0019-9958(65)90426-2","relationship":"formalizes"}]}