Linearity in Higher-Order Recursion Schemes

Watch a 24-minute conference presentation from POPL 2018 exploring how linear types can enhance Higher-Order Recursion Schemes (HORS) for program verification. Discover two new frameworks that combine non-linear and linear types: a λY-calculus variant and Linear HORS (LHORS). Learn about the polynomial-time translations between these equivalent systems and understand how Linear Nested Alternating Parity Tree Automata (LNAPTA) enable model-checking of LHORS. Examine how complexity depends on linear order and linear depth parameters, with the key finding that LNAPTA model-checking of LHORS has n-EXPTIME-complete complexity for linear order n when linear depth is fixed. See practical applications through case studies of MSO model-checking on RSFD/HORSC systems and call-by-value resource verification, demonstrating how LHORS translations achieve optimal complexity bounds compared to traditional HORS approaches.