Krivine machines and higher-order schemes
DOI10.1016/J.IC.2014.07.012zbMATH Open1309.68073OpenAlexW2057225506MaRDI QIDQ476196FDOQ476196
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
Recommendations
parity gameshigher-order model checkingKrivine machinemonadic second order logicsimply typed lambda-calculus
Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)
Cites Work
- LCF considered as a programming language
- Title not available (Why is that?)
- The IO- and OI-hierarchies
- An automata-theoretical characterization of the OI-hierarchy
- Title not available (Why is that?)
- Pushdown processes: Games and model-checking
- Title not available (Why is that?)
- A call-by-name lambda-calculus machine
- On the correctness of the Krivine machine
- The limits of decidability for first order logic on CPDA graphs
- 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
- 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
- IO vs OI in higher-order recursion schemes
Cited In (9)
- Recursion schemes and the WMSO+U logic
- Title not available (Why is that?)
- 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)
