Types and higher-order recursion schemes for verification of higher-order programs

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

Recommendations

Model checking higher-order programs
Model-checking higher-order programs with recursive types
Saturation-Based Model Checking of Higher-Order Recursion Schemes.
Verification of tree-processing programs via higher-order model checking
Model checking and functional program transformations

Cited in

(46)

Herbrand's theorem as higher order recursion
scientific article; zbMATH DE number 1086721 (Why is no real title available?)
Types and trace effects of higher order programs
Counterexample-guided partial bounding for recursive function synthesis
General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
The Complexity of the Diagonal Problem for Recursion Schemes
Model-checking higher-order programs with recursive types
Strictness analysis via abstract interpretation for recursively defined types
Pattern eliminating transformations
Parameterized recursive refinement types for automated program verification
Domains for Higher-Order Games
Propositional dynamic logic for higher-order functional programs
Efficient Verified Programs in a Type Theory with Mixed Constructivity
scientific article; zbMATH DE number 7561694 (Why is no real title available?)
Model checking higher-order programs
Higher-order multi-parameter tree transducers and recursion schemes for program verification
scientific article; zbMATH DE number 7029315 (Why is no real title available?)
On the termination problem for probabilistic higher-order recursive programs
Verifying higher-order functional programs with pattern-matching algebraic data types
Modular and automated type-soundness verification for language extensions
On first-order logic and CPDA graphs
Almost every simply typed \(\lambda\)-term has a long \(\beta\)-reduction sequence
Verification of tree-processing programs via higher-order model checking
Higher-order program verification and language-based security (extended abstract)
The mu-calculus and Model Checking
General decidability results for asynchronous shared-memory programs: higher-order and beyond
Language-based program verification via expressive types
Krivine machines and higher-order schemes
Partial bounding for recursive function synthesis
Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
Verification of Higher-Order Computation: A Game-Semantic Approach
On the relationship between higher-order recursion schemes and higher-order fixpoint logic
Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
Probabilistic verification beyond context-freeness
Type and behaviour reconstruction for higher-order concurrent programs
Monoid-based approach to the inclusion problem on superdeterministic pushdown automata
Model checking and functional program transformations
Higher order symbolic execution for contract verification and refutation
A model for behavioural properties of higher-order programs
Typestate verification: abstraction techniques and complexity results
Crowfoot: A Verifier for Higher-Order Store Programs
A bounded model checking technique for higher-order programs
A temporal logic for higher-order functional programs
Streett Automata Model Checking of Higher-Order Recursion Schemes
Functional programs as compressed data
Polynomial-time inverse computation for accumulative functions with multiple data traversals

This page was built for publication: Types and higher-order recursion schemes for verification of higher-order programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261537)