Model Checking Higher-Order Programs

DOI10.1145/2487241.2487246zbMath1281.68157OpenAlexW2036753951MaRDI QIDQ5395718

Naoki Kobayashi

Publication date: 17 February 2014

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2487241.2487246

zbMATH Keywords

model checkingtype systemshigher-order recursion schemes

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items (17)

Unnamed Item ⋮ A Nonstandard Functional Programming Language ⋮ Higher-Order Model Checking in Direct Style ⋮ Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation ⋮ Recursion Schemes and the WMSO+U Logic ⋮ Typing Weak MSOL Properties ⋮ Cost Automata, Safe Schemes, and Downward Closures ⋮ Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable ⋮ Functional programs as compressed data ⋮ Unnamed Item ⋮ Termination criteria for tree automata completion ⋮ Unnamed Item ⋮ Automata, Logic and Games for the $$\lambda $$ -Calculus ⋮ Unnamed Item ⋮ Streett Automata Model Checking of Higher-Order Recursion Schemes ⋮ Unnamed Item ⋮ Exact bounds for acyclic higher-order recursion schemes

Uses Software

• SLAM
• OCaml
• CDuce

This page was built for publication: Model Checking Higher-Order Programs