A type system describing unboundedness

DOI10.23638/DMTCS-22-4-2MaRDI QIDQ3386622zbMATH OpenOpenAlexFDO

Authors Paweł Parys

Publication date 5 January 2021

Full work available at URL https://dmtcs.episciences.org/6716

zbMATH Keywords

higher-order recursion schemesintersection typesreflectionsimultaneous-unboundedness problem

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Automata and formal grammars in connection with logical questions (03D05) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Formal languages and automata (68Q45)

Recommendations

• The Complexity of the Diagonal Problem for Recursion Schemes
• The diagonal problem for higher-order recursion schemes is decidable
• Unboundedness and downward closures of higher-order pushdown automata
• Type reconstruction with recursive types and atomic subtyping
• Untyped Recursion Schemes and Infinite Intersection Types

Cited in

(4)

• The Caucal hierarchy: interpretations in the (W)MSO+\(\mathsf{U}\) logic
• Mathematics of Program Construction
• Cost Automata, Safe Schemes, and Downward Closures
• Extending the WMSO+U logic with quantification over tuples

This page was built for publication: A type system describing unboundedness

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