A model for behavioural properties of higher-order programs

DOI10.4230/LIPICS.CSL.2015.229MaRDI QIDQ5351960zbMATH OpenOpenAlexFDO

Authors S. Salvati, Igor Walukiewicz

Publication date 31 August 2017

Full work available at URL https://hal.science/hal-01145494

zbMATH Keywords

monadic second-order logicsemantic modelssimply typed lambda-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Model checking higher-order programs
• Evaluation is MSOL-compatible
• Types and higher-order recursion schemes for verification of higher-order programs

Cited in

(13)

• Finitary semantics of linear logic and higher-order model-checking
• Evaluation is MSOL-compatible
• Recursion schemes and the WMSO+U logic
• scientific article; zbMATH DE number 2003154 (Why is no real title available?)
• Recursion schemes, the MSO logic, and the \textsf{U} quantifier
• Domains for Higher-Order Games
• Quantitative Behavioural Reasoning for Higher-order Effectful Programs
• Cost Automata, Safe Schemes, and Downward Closures
• LambdaY-calculus with priorities
• On the complexity of multi-pushdown games
• Cost automata, safe schemes, and downward closures
• Extending the WMSO+U logic with quantification over tuples
• Higher-order model checking step by step

This page was built for publication: A model for behavioural properties of higher-order programs

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