I know due to the Curry-Howard correspondence that proofs in intuitionistic logic can be mapped into programs in a programming language.
I also know that there is a correspondence between classes of different formal languages and the machines that can accept them. With Turing Machines sitting at the top accepting Unrestricted Grammars and with PDA and FSA's accepting more restrictive classes of languages.
My question is are there less expressive logical systems that correspond to Type-1, 2 and 3 grammars?
Purely as a speculation I would expect FSA and boolean logic to have a correspondence.
Quoting W. Thomas [3], the following results hold.
Theorem [1, 2] A language is regular if and only if it is definable in monadic second order of the successor.
A relation $R \subseteq \{1, \ldots, n\}$ is a matching if it contains only pairs $(i, j)$ with $i < j$ such that each position $i$ belongs to at most one pair in $R$, and there are no "crossings" between pairs (i.e. for $(i,j), (k, \ell) \in R$, $i < k < j$ implies $i < k < \ell < j$).
Theorem [3] A language is context-free if and only if it is definable in existential second-order logic where the seond-order variables range only over matchings.
[1] J. R. Büchi, Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math. 6 (1960), 66--92.
[2] C. C. Elgot, Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc. 98 (1961), 21--51.
[3] C. Lautemann, T. Schwentick, D. Thérien, Logics for context-free languages. Computer science logic (Kazimierz, 1994), 205--216, Lecture Notes in Comput. Sci. 933, Springer, Berlin, 1995.
[4] W. Thomas, Languages, automata, and logic. Handbook of formal languages, Vol. 3, 389--455, Springer, Berlin, 1997.