Name
Abstract | ||
|---|---|---|
We present subsingleton logic as a very small fragment of linear logic containing only (oplus ), (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. |
Year | Venue | Field |
|---|---|---|
2016 | APLAS | Subsequential limit,Discrete mathematics,Inverse,Deterministic finite automaton,Computer science,Sequent calculus,Theoretical computer science,Finite-state machine,Turing machine,Homomorphism,Linear logic |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
7 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Henry DeYoung | 1 | 69 | 4.74 |
| Frank Pfenning | 2 | 3376 | 265.34 |