Verifying higher-order functional programs with pattern-matching algebraic data types
From MaRDI portal
Publication:5408579
DOI10.1145/1926385.1926453zbMath1284.68193OpenAlexW4252251463MaRDI QIDQ5408579
Chih-Hao Luke Ong, S. J. Ramsay
Publication date: 10 April 2014
Published in: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1926385.1926453
Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (21)
Unnamed Item ⋮ Counterexample-guided partial bounding for recursive function synthesis ⋮ Higher-Order Model Checking in Direct Style ⋮ Unnamed Item ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Typing Weak MSOL Properties ⋮ Unnamed Item ⋮ Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable ⋮ Parameterized recursive refinement types for automated program verification ⋮ Lifting numeric relational domains to algebraic data types ⋮ Higher order symbolic execution for contract verification and refutation ⋮ Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence ⋮ Modular Verification of Higher-Order Functional Programs ⋮ Herbrand's theorem as higher order recursion ⋮ On first-order logic and CPDA graphs ⋮ Verification of tree-processing programs via higher-order mode checking ⋮ Termination criteria for tree automata completion ⋮ Automata, Logic and Games for the $$\lambda $$ -Calculus ⋮ Streett Automata Model Checking of Higher-Order Recursion Schemes ⋮ Unnamed Item ⋮ Pattern eliminating transformations
This page was built for publication: Verifying higher-order functional programs with pattern-matching algebraic data types
