Krivine machines and higher-order schemes

DOI10.1016/j.ic.2014.07.012zbMath1309.68073OpenAlexW2057225506MaRDI QIDQ476196

Sylvain Salvati, Igor Walukiewicz

Publication date: 28 November 2014

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2014.07.012

zbMATH Keywords

parity gameshigher-order model checkingKrivine machinemonadic second order logicsimply typed lambda-calculus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items (5)

Recursion Schemes and the WMSO+U Logic ⋮ Cost Automata, Safe Schemes, and Downward Closures ⋮ Unnamed Item ⋮ Krivine Machines and Higher-Order Schemes ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The IO- and OI-hierarchies
• LCF considered as a programming language
• Pushdown processes: Games and model-checking
• A call-by-name lambda-calculus machine
• On the correctness of the Krivine machine
• Collapsible Pushdown Automata and Labeled Recursion Schemes: Equivalence, Safety and Effective Selection
• Krivine Machines and Higher-Order Schemes
• Collapsible Pushdown Graphs of Level 2 are Tree-Automatic
• A Saturation Method for Collapsible Pushdown Systems
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• An automata-theoretical characterization of the OI-hierarchy
• Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata
• Types and higher-order recursion schemes for verification of higher-order programs
• Using Models to Model-Check Recursive Schemes
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
• Typed Lambda Calculi and Applications
• Automata, Languages and Programming

This page was built for publication: Krivine machines and higher-order schemes