General criteria for minimal models of streaming transducers are established, yielding effective minimization for variants of streaming string-to-tree transducers that build terms at leaves or roots.
In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Com- puter Science
4 Pith papers cite this work. Polarity classification is still indexing.
citation-role summary
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
A bijection between a subclass of appending streaming string transducers and bimachines enables Ptime register minimization and NP minimization for states and registers, extended via asynchronous bimachines to prove NP-completeness of register minimization with fixed underlying automaton.
Presents solvers for contortion (via poset maps for Dedekind/De Morgan) and Kan problems (via CSP) in cubical type theory, implemented in Haskell and demonstrated on Eckmann-Hilton.
Shallow embedding of type theory into Agda is injective up to definitional equality via a syntactic translation model, with implementation hiding ensuring no illegal propositional equalities arise.
citing papers explorer
-
Minimization of Streaming Transducers
General criteria for minimal models of streaming transducers are established, yielding effective minimization for variants of streaming string-to-tree transducers that build terms at leaves or roots.
-
Minimizing Streaming String Transducers: An algebraic approach
A bijection between a subclass of appending streaming string transducers and bimachines enables Ptime register minimization and NP minimization for states and registers, extended via asynchronous bimachines to prove NP-completeness of register minimization with fixed underlying automaton.
-
Automating Boundary Filling in Cubical Type Theories
Presents solvers for contortion (via poset maps for Dedekind/De Morgan) and Kan problems (via CSP) in cubical type theory, implemented in Haskell and demonstrated on Eckmann-Hilton.
-
Shallow Embedding of Type Theory is Morally Correct
Shallow embedding of type theory into Agda is injective up to definitional equality via a syntactic translation model, with implementation hiding ensuring no illegal propositional equalities arise.