Types and higher-order recursion schemes for verification of higher-order programs
From MaRDI portal
Publication:5261537
DOI10.1145/1480881.1480933zbMath1315.68099OpenAlexW2141505892MaRDI QIDQ5261537
Publication date: 3 July 2015
Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.217.8532
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
Counterexample-guided partial bounding for recursive function synthesis, The mu-calculus and Model Checking, General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond, Typing Weak MSOL Properties, Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable, Higher order symbolic execution for contract verification and refutation, Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence, Krivine machines and higher-order schemes, Herbrand's theorem as higher order recursion, Polynomial-time inverse computation for accumulative functions with multiple data traversals, Functional programs as compressed data, On first-order logic and CPDA graphs, Unnamed Item, General decidability results for asynchronous shared-memory programs: higher-order and beyond, Monoid-Based Approach to the Inclusion Problem on Superdeterministic Pushdown Automata, Unnamed Item, Domains for Higher-Order Games, Streett Automata Model Checking of Higher-Order Recursion Schemes, Unnamed Item, The Complexity of the Diagonal Problem for Recursion Schemes, Pattern eliminating transformations
