Skip to Main content Skip to Navigation
Reports

Krivine machines and higher-order schemes

Sylvain Salvati 1, 2 Igor Walukiewicz 2
1 SIGNES - Linguistic signs, grammar and meaning: computational logic for natural language
Université Sciences et Technologies - Bordeaux 1, Inria Bordeaux - Sud-Ouest, École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), CNRS - Centre National de la Recherche Scientifique : UMR5800
Abstract : We propose a new approach to analysing higher-order recursive schemes. Many results in the literature use automata models generalising pushdown automata, most notably higher-order pushdown automata with collapse (CPDA). Instead, we propose to use the Krivine machine model. Compared to CPDA, this model is closer to lambda-calculus, and incorporates nicely many invariants of computations, as for example the typing information. The usefulness of the proposed approach is demonstrated with new proofs of two central results in the field: the decidability of the local and global model checking problems for higher-order schemes with respect to the mu-calculus.
Document type :
Reports
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00589407
Contributor : Sylvain Salvati <>
Submitted on : Thursday, April 28, 2011 - 8:48:25 PM
Last modification on : Thursday, February 11, 2021 - 2:52:01 PM
Long-term archiving on: : Thursday, March 30, 2017 - 9:56:05 AM

File

hpda-dec.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00589407, version 1

Collections

Citation

Sylvain Salvati, Igor Walukiewicz. Krivine machines and higher-order schemes. [Research Report] 2011, pp.17. ⟨inria-00589407⟩

Share

Metrics

Record views

288

Files downloads

348