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.
Type de document :
Rapport
[Research Report] 2011, pp.17
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00589407
Contributeur : Sylvain Salvati <>
Soumis le : jeudi 28 avril 2011 - 20:48:25
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13
Document(s) archivé(s) le : jeudi 30 mars 2017 - 09:56:05

Fichier

hpda-dec.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

190

Téléchargements de fichiers

98