On average-case hardness of higher-order model checking

DOI10.4230/LIPICS.FSCD.2020.21MaRDI QIDQ6854414zbMATH OpenFDO

Authors Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

Publication date 24 February 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2020.21

zbMATH Keywords

average-case complexityhigher-order model checkingintersection type system

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX) Theory of computing (68Qxx)

Cites work

• A conjunctive type system for useless-code elimination
• A type-directed abstraction refinement approach to higher-order model checking
• Almost every simply typed -term has a long -reduction sequence
• Analytic combinatorics
• Asymptotically almost all \lambda-terms are strongly normalizing
• Automata, logics, and infinite games. A guide to current research
• Complexity of model checking recursion schemes for fragments of the modal mu-calculus
• scientific article; zbMATH DE number 5081744 (Why is no real title available?)
• scientific article; zbMATH DE number 7029315 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• Krivine machines and higher-order schemes
• Model checking higher-order programs
• On average-case hardness of higher-order model checking
• On the \(\lambda Y\) calculus
• On the likelihood of normalization in combinatory logic
• Recursive schemes, Krivine machines, and collapsible pushdown automata
• Refinement types for program analysis
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Type-based useless-variable elimination
• Types and higher-order recursion schemes for verification of higher-order programs
• Verifying higher-order functional programs with pattern-matching algebraic data types

Cited in

(1)

• On average-case hardness of higher-order model checking

This page was built for publication: On average-case hardness of higher-order model checking

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