We gratefully acknowledge support from
the Simons Foundation and member institutions.

Formal Languages and Automata Theory

New submissions

[ total of 7 entries: 1-7 ]
[ showing up to 1000 entries per page: fewer | more ]

New submissions for Fri, 21 Jan 22

[1]  arXiv:2201.08275 [pdf, ps, other]
Title: The Different Shades of Infinite Session Types
Comments: 51 pages, 12 figures
Subjects: Programming Languages (cs.PL); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)

Many type systems include infinite types. In session type systems, which are the focus of this paper, infinite types are important because they allow the specification of communication protocols that are unbounded in time. Usually infinite session types are introduced as simple finite-state expressions $\mathsf{rec}\, X.T$ or by non-parametric equational definitions $X\doteq T$. Alternatively, some systems of label- or value-dependent session types go beyond simple recursive types. However, leaving dependent types aside, there is a much richer world of infinite session types, ranging through various forms of parametric equational definitions, all the way to arbitrary infinite types in a coinductively defined space. We study infinite session types across a spectrum of shades of grey on the way to the bright light of general infinite types. We identify four points on the spectrum, characterised by different styles of equational definitions, and show that they form a strict hierarchy by establishing bidirectional correspondences with classes of automata: finite-state, 1-counter, pushdown and 2-counter. This allows us to establish decidability and undecidability results for the problems of type formation, type equivalence and duality in each class of types. We also consider previous work on context-free session types (and extend it to higher-order) and nested session types, and locate them on our spectrum of infinite types.

Replacements for Fri, 21 Jan 22

[2]  arXiv:1908.11642 (replaced) [pdf, ps, other]
Title: Weight Annotation in Information Extraction
Subjects: Databases (cs.DB); Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
[3]  arXiv:2007.03249 (replaced) [pdf, ps, other]
Title: Agafonov's Proof of Agafonov's Theorem: A Modern Account and New Insights
Authors: Thomas Seiller (CNRS, LIPN), Jakob Simonsen (DIKU)
Subjects: Discrete Mathematics (cs.DM); Formal Languages and Automata Theory (cs.FL); Probability (math.PR)
[4]  arXiv:2009.04821 (replaced) [pdf, ps, other]
Title: Pushdown and Lempel-Ziv Depth
Comments: Definition of Pushdown Depth (Def 4.1) changed to remove the ambiguity in the old definition. Proofs have been altered from the previous version to reflect this change, but the results have remined the same
Subjects: Computational Complexity (cs.CC); Formal Languages and Automata Theory (cs.FL)
[5]  arXiv:2009.12225 (replaced) [pdf, ps, other]
Title: Pebble-Depth
Comments: arXiv admin note: substantial text overlap with arXiv:2009.04821
Subjects: Computational Complexity (cs.CC); Formal Languages and Automata Theory (cs.FL)
[6]  arXiv:2105.06723 (replaced) [pdf, other]
Title: Bounded Reachability Problems are Decidable in FIFO Machines
Subjects: Logic in Computer Science (cs.LO); Formal Languages and Automata Theory (cs.FL)
[7]  arXiv:2112.14499 (replaced) [pdf, ps, other]
Title: Decidable problems in substitution shifts
Subjects: Dynamical Systems (math.DS); Formal Languages and Automata Theory (cs.FL)
[ total of 7 entries: 1-7 ]
[ showing up to 1000 entries per page: fewer | more ]

Disable MathJax (What is MathJax?)

Links to: arXiv, form interface, find, cs, recent, 2201, contact, help  (Access key information)