@inproceedings{10.1007/978-3-319-47958-3_1,
    Abstract = {We present subsingleton logic as a very small fragment of linear logic containing only {\$}{\$}{\backslash}oplus {\$}{\$}, {\$}{\$}{\backslash}mathbf {\{}1{\}}{\$}{\$}, least fixed points and allowing circular proofs. We show that cut-free proofs in this logic are in a Curry--Howard correspondence with subsequential finite state transducers. Constructions on finite state automata and transducers such as composition, complement, and inverse homomorphism can then be realized uniformly simply by cut and cut elimination. If we freely allow cuts in the proofs, they correspond to a well-typed class of machines we call linear communicating automata, which can also be seen as a generalization of Turing machines with multiple, concurrently operating read/write heads.},
    Address = {Cham},
    Author = {DeYoung, Henry and Pfenning, Frank},
    BookTitle = {Programming Languages and Systems},
    Editor = {Igarashi, Atsushi},
    File = {Substructural Proofs as Automata - aplas16-talk - a - z.pdf},
    ISBN = {978-3-319-47958-3},
    Pages = {3--22},
    Publisher = {Springer International Publishing},
    Title = {Substructural Proofs as Automata},
    Year = {2016},
    date-added = {2020-07-08 16:50:16 +0200},
    date-modified = {2020-07-08 16:50:16 +0200},
    file-2 = {Substructural Proofs as Automata - aplas16 - a - z.pdf},
    doi = {10.1007/978-3-319-47958-3_1}
}

@inproceedings{10.1007/978-3-319-47958-3_1, Abstract = {We present subsingleton logic as a very small fragment of linear logic containing only {\$}{\$}{\backslash}oplus {\$}{\$}, {\$}{\$}{\backslash}mathbf {{}1{}}{\$}{\$}, least fixed points and allowing circular proofs. We show that cut-free proofs in this logic are in a Curry--Howard correspondence with subsequential finite state transducers. Constructions on finite state automata and transducers such as composition, complement, and inverse homomorphism can then be realized uniformly simply by cut and cut elimination. If we freely allow cuts in the proofs, they correspond to a well-typed class of machines we call linear communicating automata, which can also be seen as a generalization of Turing machines with multiple, concurrently operating read/write heads.}, Address = {Cham}, Author = {DeYoung, Henry and Pfenning, Frank}, BookTitle = {Programming Languages and Systems}, Editor = {Igarashi, Atsushi}, File = {Substructural Proofs as Automata - aplas16-talk - a - z.pdf}, ISBN = {978-3-319-47958-3}, Pages = {3--22}, Publisher = {Springer International Publishing}, Title = {Substructural Proofs as Automata}, Year = {2016}, date-added = {2020-07-08 16:50:16 +0200}, date-modified = {2020-07-08 16:50:16 +0200}, file-2 = {Substructural Proofs as Automata - aplas16 - a - z.pdf}, doi = {10.1007/978-3-319-47958-3_1} }