pith. machine review for the scientific record. sign in

arxiv: 2605.03928 · v1 · submitted 2026-05-05 · 💻 cs.FL · cs.LO

Recognition: 3 theorem links

· Lean Theorem

Tree transducers of linear size-to-height increase (and the additive conjunction of linear logic)

Charles Peyrat, L\^e Th\`anh D\~ung Nguy\^en, Luc Dartois

Authors on Pith no claims yet

Pith reviewed 2026-05-08 17:45 UTC · model grok-4.3

classification 💻 cs.FL cs.LO
keywords tree transducersHennie machineslinear size-to-height increasemacro tree transducersMSO transductionslinear lambda calculusadditive conjunctiongame semantics
0
0 comments X

The pith

Tree-to-tree Hennie machines compute exactly the functions with linear size-to-height increase.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines tree-to-tree Hennie machines as tree-walking transducers that rewrite node labels while obeying a bounded-visit rule. These machines generate tree functions whose output size grows linearly with input height, a property that places them strictly above regular tree functions yet below full MSO set interpretations. The authors prove closure under precomposition by linear-size macro tree transducers and postcomposition by linear-height ones, which implies that the machines contain the entire composition hierarchy of linear-height-increase macro tree transducers and that this hierarchy is strict. They also supply an equivalent definition via a linear typed lambda calculus whose output encoding uses additive tuples rather than the multiplicative structure typical of MSO characterizations.

Core claim

Tree-to-tree Hennie machines, defined as tree-walking transducers with label rewriting and bounded visits, compute precisely the tree-to-tree functions of linear size-to-height increase. This class lies between linear-height-increase macro tree transducers and MSO set interpretations, is closed under the indicated pre- and post-compositions, contains the full strict hierarchy of linear-height-increase macro tree transducers, and admits an equivalent characterization in the linear lambda calculus that encodes output trees by additive tuples.

What carries the argument

The bounded-visit label-rewriting tree-walking transducer, equivalently characterized by linear lambda terms using additive tuples for output encoding.

If this is right

  • The composition hierarchy of macro tree transducers with linear height increase is strict.
  • The class remains closed under precomposition by any linear-size-increase macro tree transducer.
  • The class remains closed under postcomposition by any linear-height-increase macro tree transducer.
  • Game semantics suffice to establish equivalence between the transducer model and the linear lambda calculus with additive tuples.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Additive conjunction in linear logic appears to be the precise connective needed to track size increase relative to height in tree encodings.
  • The same game-semantics technique may extend to other restricted-increase transducer classes beyond trees.
  • Decidability or complexity results known for linear lambda terms could transfer directly to questions about these tree functions.

Load-bearing premise

The bounded-visit restriction on tree-walking transducers is assumed to enforce exactly the linear size-to-height increase property.

What would settle it

A concrete tree function with linear size-to-height increase that cannot be realized by any bounded-visit label-rewriting tree-walking transducer, or equivalently a linear lambda term with additive tuples that computes a function outside the class.

read the original abstract

We investigate a natural generalization to trees of Hennie machines, a known automaton model for regular string functions. Tree-to-tree Hennie machines are tree-walking tree transducers with the ability to rewrite the node labels of their input tree, subject to a bounded visit restriction. Interestingly, they do not merely compute regular tree functions (i.e. MSO transductions), but a larger class of functions with linear size-to-height increase (LSHI). We prove that this class sits between LSHI macro tree transducers (MTTs) and MSO set interpretations. To argue for its robustness, we show that it is closed under precomposition (resp. postcomposition) by MTTs of linear size (resp. height) increase. As a consequence, it contains the entire composition hierarchy of MTTs of linear height increase; we also prove that this composition hierarchy is strict. Finally, we give an alternative characterization of this function class based on a lambda-calculus with linear types. The key difference with similar characterizations of MSO transductions is the use of additive tuples in the encoding of output trees. Our equivalence proof, using game semantics / geometry of interaction, is heavily inspired by an analogous result on higher-order recursion schemes.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces tree-to-tree Hennie machines as bounded-visit tree-walking transducers with label rewriting. It claims these compute exactly the tree functions with linear size-to-height increase (LSHI), that this class lies strictly between LSHI macro tree transducers and MSO set interpretations, that it is closed under precomposition by linear-size MTTs and postcomposition by linear-height MTTs, that it contains the full (and strict) composition hierarchy of linear-height-increase MTTs, and that it admits an equivalent characterization via a linear lambda-calculus with additive tuples, proved using game semantics inspired by recursion-scheme results.

Significance. If the central equivalences hold, the work defines a robust, natural intermediate class of tree functions with linear resource bounds, equipped with useful closure properties and a logical characterization that differs from MSO transductions precisely by the use of additive conjunction. The strictness proof for the MTT composition hierarchy and the game-semantics equivalence are notable strengths that could inform resource-sensitive tree transformations and connections between automata and linear logic.

major comments (2)
  1. [Definition of Hennie machines and main equivalence theorem] Definition of tree-to-tree Hennie machines and the LSHI equivalence theorem: the claim that the bounded-visit restriction plus label rewriting yields precisely linear size-to-height increase must explicitly rule out super-linear blow-ups arising from rewriting on high-arity nodes or deep label changes; without a concrete size bound or induction argument addressing non-uniform arities, the positioning between LSHI MTTs and MSO interpretations does not yet follow.
  2. [Lambda-calculus characterization and game-semantics proof] Game-semantics equivalence to the linear lambda-calculus with additive tuples: the proof must confirm that the additive-tuple encoding of output trees works for arbitrary tree ranks and label alphabets without hidden restrictions, otherwise the claimed equivalence to the transducer model (and therefore the closure and hierarchy results) may hold only in a restricted fragment.
minor comments (2)
  1. [Abstract] The abstract introduces LSHI without a one-sentence formal definition or reference to the precise size/height functions used; adding this would improve readability.
  2. [Preliminaries] Notation for visit bounds, size, and height should be introduced with a small running example before the main theorems.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. We address each major comment below and will revise the manuscript to improve explicitness of the arguments.

read point-by-point responses

  1. Referee: [Definition of Hennie machines and main equivalence theorem] Definition of tree-to-tree Hennie machines and the LSHI equivalence theorem: the claim that the bounded-visit restriction plus label rewriting yields precisely linear size-to-height increase must explicitly rule out super-linear blow-ups arising from rewriting on high-arity nodes or deep label changes; without a concrete size bound or induction argument addressing non-uniform arities, the positioning between LSHI MTTs and MSO interpretations does not yet follow.

    Authors: We agree that greater explicitness is needed. The proof of the main equivalence (Theorem 3.1) proceeds by induction on input-tree height, using the bounded-visit restriction (at most k visits per node for fixed k) and the finite label alphabet to bound the local size increase per visit by a constant independent of arity. Because each node is visited only constantly often and rewriting replaces a label with one of finitely many others, the total output size remains linear in input height even for non-uniform arities. We will insert an auxiliary lemma (new Lemma 3.2) that states this concrete linear bound before the induction, thereby ruling out super-linear blow-ups and making the placement between LSHI MTTs and MSO interpretations fully rigorous. revision: partial

  2. Referee: [Lambda-calculus characterization and game-semantics proof] Game-semantics equivalence to the linear lambda-calculus with additive tuples: the proof must confirm that the additive-tuple encoding of output trees works for arbitrary tree ranks and label alphabets without hidden restrictions, otherwise the claimed equivalence to the transducer model (and therefore the closure and hierarchy results) may hold only in a restricted fragment.

    Authors: The game-semantics construction in Section 5 is formulated for arbitrary finite ranks and finite label alphabets; the additive-tuple encoding represents output branching via the additive conjunction of linear logic and does not depend on a fixed maximum arity or on particular label sets. The correspondence between plays and transducer runs is proved by induction on the structure of the linear lambda term, which is independent of the concrete tree signature. We will add a short paragraph at the start of Section 5 explicitly stating the generality of the construction and confirming that the equivalence therefore transfers to the full class of tree-to-tree Hennie machines. revision: partial

Circularity Check

0 steps flagged

No circularity detected; derivation chain is self-contained

full rationale

The paper defines tree-to-tree Hennie machines directly as tree-walking transducers with label rewriting and bounded visits, then proves via independent arguments that they compute exactly the LSHI class (positioned between LSHI MTTs and MSO set interpretations), establishes closure under pre/post-composition by linear MTTs, shows the MTT composition hierarchy is strict and contained, and gives a separate lambda-calculus characterization with additive tuples via game semantics. The inspiration from prior recursion-scheme results is acknowledged but does not reduce any central claim to a self-citation or definitional tautology. No quoted steps exhibit self-definition, fitted inputs renamed as predictions, or load-bearing self-references; all results are presented as derived from the model definitions and explicit proofs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The claims rest on standard background definitions from automata theory (tree-walking transducers, MSO) and linear logic (additive conjunction, game semantics), plus the new machine model itself. No numerical free parameters or data-fitting appear.

axioms (2)
  • standard math Standard definitions and closure properties of tree transducers and MSO logic on trees
    The positioning between LSHI MTTs and MSO set interpretations relies on these established notions.
  • standard math Game semantics and geometry of interaction techniques apply to the linear lambda calculus encoding
    The equivalence proof is described as heavily inspired by analogous results on higher-order recursion schemes.
invented entities (1)
  • Tree-to-tree Hennie machines no independent evidence
    purpose: A new transducer model that rewrites node labels under bounded visits to achieve LSHI functions
    This is the central new automaton model introduced and studied in the paper.

pith-pipeline@v0.9.0 · 5536 in / 1657 out tokens · 37718 ms · 2026-05-08T17:45:37.135804+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

Reference graph

Works this paper leans on

51 extracted references · 44 canonical work pages · 1 internal anchor

  1. [1]

    Verifying unboundedness via amalgamation

    Ashwani Anand, Sylvain Schmitz, Lia Sch \" u tze, and Georg Zetzsche. Verifying unboundedness via amalgamation. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024 , pages 4:1--4:15. ACM , 2024. https://doi.org/10.1145/3...

    work page doi:10.1145/3661814.3662133 2024

  2. [2]

    Transducers with origin information

    Mikołaj Bojańczyk. Transducers with origin information. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II , volume 8573 of Lecture Notes in Computer Science , pages 26--37. Springe...

    work page doi:10.1007/978-3-662-43951-7_3 2014

  3. [3]

    Transducers of polynomial growth (invited talk)

    Mikołaj Bojańczyk. Transducers of polynomial growth (invited talk). In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , pages 1:1--1:27. ACM , 2022. https://doi.org/10.1145/3531130.3533326 doi:10.1145/3531130.3533326

    work page doi:10.1145/3531130.3533326 2022

  4. [4]

    Folding interpretations

    Mikołaj Bojańczyk. Folding interpretations. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023 , pages 1--13. IEEE , 2023. https://doi.org/10.1109/LICS56636.2023.10175796 doi:10.1109/LICS56636.2023.10175796

    work page doi:10.1109/lics56636.2023.10175796 2023

  5. [5]

    String-to-string interpretations with polynomial-size output

    Mikołaj Bojańczyk, Sandra Kiefer, and Nathan Lhote. String-to-string interpretations with polynomial-size output. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece , pages 106:1--106:14, 2019. https://doi.org/10.4230/LIPIcs.ICALP.2019.106 doi:10.4230/LIPIcs.ICALP.2019.106

    work page doi:10.4230/lipics.icalp.2019.106 2019

  6. [6]

    Linearity in Higher -order Recursion Schemes

    Pierre Clairambault, Charles Grellois, and Andrzej Murawski. Linearity in Higher -order Recursion Schemes . Proceedings of the ACM on Programming Languages , 2(POPL):39:1--39:29, December 2017. https://doi.org/10.1145/3158127 doi:10.1145/3158127

    work page doi:10.1145/3158127 2017

  7. [7]

    Murawski

    Pierre Clairambault and Andrzej S. Murawski. On the Expressivity of Linear Recursion Schemes . In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science ( MFCS 2019) , volume 138 of Leibniz International Proceedings in Informatics ( LIPIcs ) , pages 50:1--50:14. Sch...

    work page doi:10.4230/lipics.mfcs.2019.50 2019

  8. [8]

    Logic and regular cost functions

    Thomas Colcombet. Logic and regular cost functions. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017 , pages 1--4. IEEE Computer Society, 2017. https://doi.org/10.1109/LICS.2017.8005061 doi:10.1109/LICS.2017.8005061

    work page doi:10.1109/lics.2017.8005061 2017

  9. [9]

    Expregular functions

    Thomas Colcombet, Nathan Lhote, and Pierre Ohlmann. Expregular functions, 2026. To appear in the proceedings of ICALP 2026. https://arxiv.org/abs/2602.21019 arXiv:2602.21019

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  10. [10]

    Transforming structures by set interpretations

    Thomas Colcombet and Christof Löding. Transforming structures by set interpretations. Logical Methods in Computer Science , 3(2), 2007. https://doi.org/10.2168/LMCS-3(2:4)2007 doi:10.2168/LMCS-3(2:4)2007

    work page doi:10.2168/lmcs-3(2:4)2007 2007

  11. [11]

    Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach

    Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach . Cambridge University Press, June 2012. https://doi.org/10.1017/cbo9780511977619 doi:10.1017/cbo9780511977619

    work page doi:10.1017/cbo9780511977619 2012

  12. [12]

    Formalising actors in linear logic

    John Darlington and Yike Guo. Formalising actors in linear logic. In Dilip Patel, Yuan Sun, and Shushma Patel, editors, Proceedings of the 1994 International Conference on Object Oriented Information Systems, OOIS 1994, London, UK, December 19-21, 1994 , pages 37--53. Springer, 1994. https://doi.org/10.1007/978-1-4471-3016-1_3 doi:10.1007/978-1-4471-3016-1_3

    work page doi:10.1007/978-1-4471-3016-1_3 1994

  13. [13]

    On reversible transducers

    Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote. On reversible transducers. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland , volume 80 of LIPIcs , pages 113:1--113:12. Schloss Dagstuhl - Leibn...

    work page doi:10.4230/lipics.icalp.2017.113 2017

  14. [14]

    Dilworth

    Robert P. Dilworth. A decomposition theorem for partially ordered sets. Annals of Mathematics , 51(1):161, January 1950. https://doi.org/10.2307/1969503 doi:10.2307/1969503

    work page doi:10.2307/1969503 1950

  15. [15]

    Optimization of string transducers

    Gaëtan Douéneau-Tabot. Optimization of string transducers . PhD thesis, Université Paris Cité, November 2023. URL: https://theses.hal.science/tel-04690881

    2023

  16. [16]

    Register Transducers Are Marble Transducers

    Gaëtan Douéneau-Tabot, Emmanuel Filiot, and Paul Gastin. Register Transducers Are Marble Transducers . In Javier Esparza and Daniel Kr \'a ľ, editors, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020) , volume 170 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 29:1--29:14, Dagstuhl, Germany, 202...

    work page doi:10.4230/lipics.mfcs.2020.29 2020

  17. [17]

    MSO definable string transductions and two-way finite-state transducers

    Joost Engelfriet and Hendrik Jan Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Transactions on Computational Logic , 2(2):216--254, April 2001. https://doi.org/10.1145/371316.371512 doi:10.1145/371316.371512

    work page doi:10.1145/371316.371512 2001

  18. [18]

    Two-way finite state transducers with nested pebbles

    Joost Engelfriet and Sebastian Maneth. Two-way finite state transducers with nested pebbles. In Krzysztof Diks and Wojciech Rytter, editors, Mathematical Foundations of Computer Science 2002, 27th International Symposium, MFCS 2002, Warsaw, Poland, August 26-30, 2002, Proceedings , volume 2420 of Lecture Notes in Computer Science , pages 234--244. Springe...

    work page doi:10.1007/3-540-45687-2_19 2002

  19. [19]

    A comparison of pebble tree transducers with macro tree transducers

    Joost Engelfriet and Sebastian Maneth. A comparison of pebble tree transducers with macro tree transducers. Acta Informatica , 39(9):613--698, 2003. https://doi.org/10.1007/s00236-003-0120-0 doi:10.1007/s00236-003-0120-0

    work page doi:10.1007/s00236-003-0120-0 2003

  20. [20]

    Macro tree translations of linear size increase are MSO definable

    Joost Engelfriet and Sebastian Maneth. Macro tree translations of linear size increase are MSO definable. SIAM Journal on Computing , 32(4):950--1006, 2003. https://doi.org/10.1137/S0097539701394511 doi:10.1137/S0097539701394511

    work page doi:10.1137/s0097539701394511 2003

  21. [21]

    Macro tree transducers

    Joost Engelfriet and Heiko Vogler. Macro tree transducers. Journal of Computer and System Sciences , 31(1):71--146, 1985. https://doi.org/10.1016/0022-0000(85)90066-2 doi:10.1016/0022-0000(85)90066-2

    work page doi:10.1016/0022-0000(85)90066-2 1985

  22. [22]

    Pushdown machines for the macro tree transducer

    Joost Engelfriet and Heiko Vogler. Pushdown machines for the macro tree transducer. Theoretical Computer Science , 42:251--368, 1986. https://doi.org/10.1016/0304-3975(86)90052-6 doi:10.1016/0304-3975(86)90052-6

    work page doi:10.1016/0304-3975(86)90052-6 1986

  23. [23]

    Word- Mappings of Level 2

    Julien Ferté, Nathalie Marin, and Géraud Sénizergues. Word- Mappings of Level 2. Theory of Computing Systems , 54(1):111--148, January 2014. https://doi.org/10.1007/s00224-013-9489-5 doi:10.1007/s00224-013-9489-5

    work page doi:10.1007/s00224-013-9489-5 2014

  24. [24]

    Lexicographic Transductions of Finite Words

    Emmanuel Filiot, Nathan Lhote, and Pierre-Alain Reynier. Lexicographic Transductions of Finite Words . In Pawe Gawrychowski, Filip Mazowiecki, and Micha Skrzypczak, editors, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) , volume 345 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 50:1--50:18,...

    work page doi:10.4230/lipics.mfcs.2025.50 2025

  25. [25]

    Note on Dilworth's decomposition theorem for partially ordered sets

    Delbert Ray Fulkerson. Note on Dilworth's decomposition theorem for partially ordered sets. Proceedings of the American Mathematical Society , 7(4):701, August 1956. https://doi.org/10.2307/2033375 doi:10.2307/2033375

    work page doi:10.2307/2033375 1956

  26. [26]

    Linear high-order deterministic tree transducers with regular look-ahead

    Paul Gallot, Aurélien Lemay, and Sylvain Salvati. Linear high-order deterministic tree transducers with regular look-ahead. In Javier Esparza and Daniel Kr \' a l', editors, 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic , volume 170 of LIPIcs , pages 38:1--38:13. Schloss...

    work page doi:10.4230/lipics.mfcs.2020.38 2020

  27. [27]

    The structure of polynomial growth for tree automata/transducers and mso set queries, 2025

    Paul Gallot, Nathan Lhote, and Lê Thành Dũng . The structure of polynomial growth for tree automata/transducers and mso set queries, 2025. https://arxiv.org/abs/2501.10270 arXiv:2501.10270

    work page arXiv 2025

  28. [28]

    Deciding linear height and linear size-to-height increase of macro tree transducers

    Paul Gallot, Sebastian Maneth, Keisuke Nakano, and Charles Peyrat. Deciding linear height and linear size-to-height increase of macro tree transducers. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors, 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn, Estonia , volume 29...

    work page doi:10.4230/lipics.icalp.2024.138 2024

  29. [29]

    Paul D. Gallot. Safety of transformations of data trees: tree transducer theory applied to a verification problem on shell scripts . PhD thesis, Université de Lille , December 2021. URL: https://theses.hal.science/tel-03773108

    2021

  30. [30]

    Semantics of linear logic and higher-order model-checking

    Charles Grellois. Semantics of linear logic and higher-order model-checking . PhD thesis, Université Paris 7, April 2016. URL: https://theses.hal.science/tel-01311150/

    2016

  31. [31]

    Converting nondeterministic two-way automata into small deterministic linear-time machines

    Bruno Guillon, Giovanni Pighizzini, Luca Prigioniero, and Daniel Pr u s a. Converting nondeterministic two-way automata into small deterministic linear-time machines. Information and Computation , 289, 2022. https://doi.org/10.1016/J.IC.2022.104938 doi:10.1016/J.IC.2022.104938

    work page doi:10.1016/j.ic.2022.104938 2022

  32. [32]

    Weight-reducing Turing machines

    Bruno Guillon, Giovanni Pighizzini, Luca Prigioniero, and Daniel Pr u s a. Weight-reducing Turing machines. Information and Computation , 292, 2023. https://doi.org/10.1016/J.IC.2023.105030 doi:10.1016/J.IC.2023.105030

    work page doi:10.1016/j.ic.2023.105030 2023

  33. [33]

    Linear-time limited automata

    Bruno Guillon and Luca Prigioniero. Linear-time limited automata. Theoretical Computer Science , 798:95--108, 2019. https://doi.org/10.1016/J.TCS.2019.03.037 doi:10.1016/J.TCS.2019.03.037

    work page doi:10.1016/j.tcs.2019.03.037 2019

  34. [34]

    Frederick C. Hennie. One-tape, off-line turing machine computations. Information and Control , 8(6):553--578, 1965. https://doi.org/10.1016/S0019-9958(65)90399-2 doi:10.1016/S0019-9958(65)90399-2

    work page doi:10.1016/s0019-9958(65)90399-2 1965

  35. [35]

    A universal modular ACTOR formalism for artificial intelligence

    Carl Hewitt, Peter Boehler Bishop, and Richard Steiger. A universal modular ACTOR formalism for artificial intelligence. In Nils J. Nilsson, editor, Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973 , pages 235--245. William Kaufmann, 1973. URL: http://ijcai.org/Proceedings/73/Papers/027B.pdf

    1973

  36. [36]

    Hillebrand and Paris C

    Gerd G. Hillebrand and Paris C. Kanellakis. On the Expressive Power of Simply Typed and Let - Polymorphic Lambda Calculi . In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science , pages 253--263. IEEE Computer Society, 1996. https://doi.org/10.1109/LICS.1996.561337 doi:10.1109/LICS.1996.561337

    work page doi:10.1109/lics.1996.561337 1996

  37. [37]

    Polyregular functions -- characterisations and refutations (invited talk)

    Sandra Kiefer. Polyregular functions -- characterisations and refutations (invited talk). In Joel D. Day and Florin Manea, editors, Developments in Language Theory - 28th International Conference, DLT 2024, G \" o ttingen, Germany, August 12-16, 2024, Proceedings , volume 14791 of Lecture Notes in Computer Science , pages 13--21. Springer, 2024. https://d...

    work page doi:10.1007/978-3-031-66159-4_2 2024

  38. [38]

    Refutations of pebble minimization via output languages, 2023

    Sandra Kiefer, Lê Thành Dũng , and Cécilia Pradic. Refutations of pebble minimization via output languages, 2023. https://arxiv.org/abs/2301.09234 arXiv:2301.09234

    work page arXiv 2023

  39. [39]

    43 years of actors: a taxonomy of actor models and their key properties

    Joeri De Koster, Tom Van Cutsem, and Wolfgang De Meuter. 43 years of actors: a taxonomy of actor models and their key properties. In Sylvan Clebsch, Travis Desell, Philipp Haller, and Alessandro Ricci, editors, Proceedings of the 6th International Workshop on Programming Based on Actors, Agents, and Decentralized Control, AGERE 2016, Amsterdam, The Nether...

    work page doi:10.1145/3001886.3001890 2016

  40. [40]

    Classes of languages and linear-bounded automata

    Sige - Yuki Kuroda. Classes of languages and linear-bounded automata. Information and Control , 7(2):207--223, 1964. https://doi.org/10.1016/S0019-9958(64)90120-2 doi:10.1016/S0019-9958(64)90120-2

    work page doi:10.1016/s0019-9958(64)90120-2 1964

  41. [41]

    Murawski, and Luke Ong

    Guanyan Li, Andrzej S. Murawski, and Luke Ong. Probabilistic verification beyond context-freeness. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , pages 33:1--33:13. ACM , 2022. https://doi.org/10.1145/3531130.3533351 doi:10.1145/3531130.3533351

    work page doi:10.1145/3531130.3533351 2022

  42. [42]

    Higher-order parity automata

    Paul-André Melliès. Higher-order parity automata. In 2017 32nd Annual ACM / IEEE Symposium on Logic in Computer Science ( LICS ) , pages 1--12, Reykjavik, Iceland, June 2017. IEEE. https://doi.org/10.1109/LICS.2017.8005077 doi:10.1109/LICS.2017.8005077

    work page doi:10.1109/lics.2017.8005077 2017

  43. [43]

    A topological and fibrational approach to higher-order automata

    Vincent Moreau. A topological and fibrational approach to higher-order automata . PhD thesis, Universit \'e Paris Cit \'e , July 2025. URL: https://theses.hal.science/tel-05428993

    2025

  44. [44]

    Implicit automata in linear logic and categorical transducer theory

    Lê Thành Dũng . Implicit automata in linear logic and categorical transducer theory . PhD thesis, Université Paris XIII (Sorbonne Paris Nord), December 2021. URL: https://theses.hal.science/tel-04132636

    2021

  45. [45]

    Implicit automata in typed -calculi I : aperiodicity in a non-commutative logic

    Lê Thành Dũng and Cécilia Pradic. Implicit automata in typed -calculi I : aperiodicity in a non-commutative logic. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, July 8-11, 2020, Saarbrücken, Germany (Virtual Conference) , volume 168 of LIPIcs , pages 135:1--13...

    work page doi:10.4230/lipics.icalp.2020.135 2020

  46. [46]

    Slightly Non-Linear Higher-Order Tree Transducers

    Lê Thành Dũng and Gabriele Vanoni. Slightly Non-Linear Higher-Order Tree Transducers . In Olaf Beyersdorff, Micha Pilipczuk, Elaine Pimentel, and Kim Thang, editors, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025) , volume 327 of Leibniz International Proceedings in Informatics (LIPIcs) , pages 68:1--68:20, Dagstuhl, G...

    work page doi:10.4230/lipics.stacs.2025.68 2025

  47. [47]

    Implicit automata in -calculi iii: affine planar string-to-string functions

    Cécilia Pradic and Ian Price. Implicit automata in -calculi iii: affine planar string-to-string functions. Electronic Notes in Theoretical Informatics and Computer Science , Volume 4 - Proceedings of MFPS XL, Dec 2024. https://doi.org/10.46298/entics.14804 doi:10.46298/entics.14804

    work page doi:10.46298/entics.14804 2024

  48. [48]

    Bounded-crossing transducers

    V \' a clav Rajlich. Bounded-crossing transducers. Information and Control , 27(4):329--335, 1975. https://doi.org/10.1016/S0019-9958(75)90159-X doi:10.1016/S0019-9958(75)90159-X

    work page doi:10.1016/s0019-9958(75)90159-x 1975

  49. [49]

    Lambda-calculus and formal language theory

    Sylvain Salvati. Lambda-calculus and formal language theory . Habilitation thesis, Université de Bordeaux, 2015. URL: https://theses.hal.science/tel-01253426

    2015

  50. [50]

    Relational presheaves, change of base and weak simulation

    Paweł Sobociński. Relational presheaves, change of base and weak simulation. Journal of Computer and System Sciences , 81(5):901–910, August 2015. https://doi.org/10.1016/j.jcss.2014.12.007 doi:10.1016/j.jcss.2014.12.007

    work page doi:10.1016/j.jcss.2014.12.007 2015

  51. [51]

    Automata theory and higher-order model-checking

    Igor Walukiewicz. Automata theory and higher-order model-checking. ACM SIGLOG News , 3(4):13--31, 2016. https://doi.org/10.1145/3026744.3026745 doi:10.1145/3026744.3026745

    work page doi:10.1145/3026744.3026745 2016