Recursion schemes and the WMSO+U logic

DOI10.4230/LIPICS.STACS.2018.53zbMATH Open1491.03010OpenAlexW2791847152MaRDI QIDQ3304152FDOQ3304152

Authors: Paweł Parys 

Publication date: 5 August 2020

Full work available at URL: https://doi.org/10.4230/LIPIcs.STACS.2018.53

Recommendations

• Weak \(\text{MSO}+U\) over infinite trees
• The Caucal hierarchy: interpretations in the (W)MSO+\(\mathsf{U}\) logic
• Weak MSO+U with path quantifiers over infinite trees
• scientific article; zbMATH DE number 6829362
• The diagonal problem for higher-order recursion schemes is decidable

zbMATH Keywords

boundednessintersection typeshigher-order recursion schemesWMSO+U logic

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Cites Work

• Weak \(\text{MSO}+U\) over infinite trees
• The IO- and OI-hierarchies
• Title not available (Why is that?)
• Indexed Grammars—An Extension of Context-Free Grammars
• Weak MSO with the unbounding quantifier
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• The first order properties of products of algebraic systems
• New algorithm for weak monadic second-order logic on inductive structures
• The monadic theory of order
• Collapsible pushdown automata and labeled recursion schemes, equivalence, safety and effective selection
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• Krivine machines and higher-order schemes
• Using models to model-check recursive schemes
• A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
• Model checking higher-order programs
• Computer Science Logic
• Title not available (Why is that?)
• Models of \(\lambda\)-calculus and the weak MSO logic
• A type-directed abstraction refinement approach to higher-order model checking
• A Note on Decidable Separability by Piecewise Testable Languages
• Unboundedness and downward closures of higher-order pushdown automata
• The diagonal problem for higher-order recursion schemes is decidable
• Logical theories and compatible operations
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Weak MSO+U with path quantifiers over infinite trees
• Simply typed fixpoint calculus and collapsible pushdown automata
• A model for behavioural properties of higher-order programs
• A unified approach to boundedness properties in MSO

Cited In (5)

• Title not available (Why is that?)
• On the termination problem for probabilistic higher-order recursive programs
• Title not available (Why is that?)
• The Caucal hierarchy: interpretations in the (W)MSO+\(\mathsf{U}\) logic
• Weak \(\text{MSO}+U\) over infinite trees

Uses Software

• TravMC2

This page was built for publication: Recursion schemes and the WMSO+U logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3304152)