Verification of Higher-Order Computation: A Game-Semantic Approach

DOI10.1007/978-3-540-78739-6_23MaRDI QIDQ5458405zbMATH OpenOpenAlexFDO

Authors

Publication date 11 April 2008

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78739-6_23

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• scientific article; zbMATH DE number 5825969
• Recursion schemes, collapsible pushdown automata and higher-order model checking
• Model checking higher-order programs
• Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)
• Types and higher-order recursion schemes for verification of higher-order programs

Cited in

(6)

• Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)
• Domains for Higher-Order Games
• Compositional higher-order model checking via -regular games over Böhm trees
• Recursion schemes, collapsible pushdown automata and higher-order model checking
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• State separation for code-based game-playing proofs

Describes a project that uses

Uses Software

• Boogie
• Spec#

This page was built for publication: Verification of Higher-Order Computation: A Game-Semantic Approach

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