Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
Krivine machines and higher-order schemes
du groupe Graphes et Logique

Date 2011-06-21  11:00-12:00
TitreKrivine machines and higher-order schemes 
Résumé(joint work with S. Salvati) 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. 
Lieusalle 76 
OrateurIgor Walukiewicz 
Emailigw@labri.fr 
UrlCNRS, LaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index