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

DOI10.1145/1480881.1480933zbMATH Open1315.68099OpenAlexW2141505892MaRDI QIDQ5261537FDOQ5261537

Naoki Kobayashi

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

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

zbMATH Keywords

model checkingtype systemhigher-order recursion scheme

Mathematics Subject Classification ID

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)

Cited In (36)

• Herbrand's theorem as higher order recursion
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Parameterized recursive refinement types for automated program verification
• Strictness analysis via abstract interpretation for recursively defined types
• Domains for Higher-Order Games
• Pattern eliminating transformations
• Propositional dynamic logic for higher-order functional programs
• Efficient Verified Programs in a Type Theory with Mixed Constructivity
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modular and automated type-soundness verification for language extensions
• On first-order logic and CPDA graphs
• Higher-order program verification and language-based security (extended abstract)
• Typing Weak MSOL Properties
• The mu-calculus and Model Checking
• General decidability results for asynchronous shared-memory programs: higher-order and beyond
• Partial bounding for recursive function synthesis
• Language-based program verification via expressive types
• Krivine machines and higher-order schemes
• Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
• Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence
• Probabilistic verification beyond context-freeness
• Type and behaviour reconstruction for higher-order concurrent programs
• Higher order symbolic execution for contract verification and refutation
• 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
• Monoid-Based Approach to the Inclusion Problem on Superdeterministic Pushdown Automata

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)