Automating relatively complete verification of higher-order functional programs

DOI10.1145/2429069.2429081zbMath1301.68182OpenAlexW2078578987MaRDI QIDQ2931785

Hiroshi Unno, Naoki Kobayashi, Tachio Terauchi

Publication date: 27 November 2014

Published in: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://tsukuba.repo.nii.ac.jp/record/29119/files/POPL2013.pdf

zbMATH Keywords

relative completenesstype inferencesoftware model checkinghigher-order programs

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Parameterized recursive refinement types for automated program verification ⋮ Modular Verification of Higher-Order Functional Programs ⋮ ICE-based refinement type discovery for higher-order functional programs ⋮ On recursion-free Horn clauses and Craig interpolation

This page was built for publication: Automating relatively complete verification of higher-order functional programs