|
|
|
Intitulé:
Krivine machines and higher-order schemes du groupe Graphes et Logique
|
Date | 2011-06-21 11:00-12:00 |
Titre | Krivine 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. |
Lieu | salle 76 |
Orateur | Igor Walukiewicz |
Email | igw@labri.fr |
Url | CNRS, LaBRI |
Aucun document lié à cet événement. RetourRetour à l'index
| |