Search

• < Previous
• 1
• Next >

---

Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems

Matthew Hague ; C. -H. Luke Ong.

Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested "stack of stacks" structure. These systems may be used to model higher-order programs and are closely related to the Caucal hierarchy of infinite graphs and safe higher-order&nbsp;[&hellip;]

---

Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus

Naoki Kobayashi ; C. -H. Luke Ong.

Ong has shown that the modal mu-calculus model checking problem (equivalently, the alternating parity tree automaton (APT) acceptance problem) of possibly-infinite ranked trees generated by order-n recursion schemes is n-EXPTIME complete. We consider two subclasses of APT and investigate the&nbsp;[&hellip;]

---

The Safe Lambda Calculus

William Blum ; C. -H. Luke Ong.

Safety is a syntactic condition of higher-order grammars that constrains occurrences of variables in the production rules according to their type-theoretic order. In this paper, we introduce the safe lambda calculus, which is obtained by transposing (and generalizing) the safety condition to the&nbsp;[&hellip;]

---