Krivine machines and higher-order schemes

DOI10.1016/J.IC.2014.07.012MaRDI QIDQ476196zbMATH OpenOpenAlexFDO

Authors S. 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)

Recommendations

• Krivine machines and higher-order schemes
• Recursive schemes, Krivine machines, and collapsible pushdown automata
• scientific article; zbMATH DE number 5825969
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• Alternating parity Krivine automata

Cites work

• scientific article; zbMATH DE number 1229489 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata
• A Saturation Method for Collapsible Pushdown Systems
• A call-by-name lambda-calculus machine
• An automata-theoretical characterization of the OI-hierarchy
• Automata, Languages and Programming
• Collapsible Pushdown Graphs of Level 2 are Tree-Automatic
• Collapsible pushdown automata and labeled recursion schemes, equivalence, safety and effective selection
• IO vs OI in higher-order recursion schemes
• Krivine machines and higher-order schemes
• LCF considered as a programming language
• On Global Model Checking Trees Generated by Higher-Order Recursion Schemes
• On the correctness of the Krivine machine
• Pushdown processes: Games and model-checking
• Recursive schemes, Krivine machines, and collapsible pushdown automata
• The IO- and OI-hierarchies
• The limits of decidability for first order logic on CPDA graphs
• Typed Lambda Calculi and Applications
• Types and higher-order recursion schemes for verification of higher-order programs
• Using models to model-check recursive schemes

Cited in

(9)

• Recursion schemes and the WMSO+U logic
• scientific article; zbMATH DE number 7199579 (Why is no real title available?)
• Cost Automata, Safe Schemes, and Downward Closures
• A type-directed negation elimination
• Krivine machines and higher-order schemes
• Strongly reducing variants of the Krivine abstract machine
• Reducing higher-order recursion scheme equivalence to coinductive higher-order constrained Horn clauses
• Krivine schemes are optimal
• Recursive schemes, Krivine machines, and collapsible pushdown automata

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

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