Automatic Termination Verification for Higher-Order Functional Programs

DOI10.1007/978-3-642-54833-8_21zbMath1347.68231OpenAlexW161537417MaRDI QIDQ5410711

Naoki Kobayashi, Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno

Publication date: 16 April 2014

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-54833-8_21

Mathematics Subject Classification ID

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

Related Items (4)

Higher-Order Model Checking in Direct Style ⋮ Parameterized recursive refinement types for automated program verification ⋮ Temporal refinements for guarded recursive types ⋮ ICE-based refinement type discovery for higher-order functional programs

Uses Software

• SLAM
• z3
• OCaml
• AProVE
• HMC

This page was built for publication: Automatic Termination Verification for Higher-Order Functional Programs