Krivine machines and higher-order schemes
| hal.structure.identifier | Linguistic signs, grammar and meaning: computational logic for natural language [SIGNES] | |
| hal.structure.identifier | Laboratoire Bordelais de Recherche en Informatique [LaBRI] | |
| dc.contributor.author | SALVATI, Sylvain | |
| hal.structure.identifier | Laboratoire Bordelais de Recherche en Informatique [LaBRI] | |
| dc.contributor.author | WALUKIEWICZ, Igor | |
| dc.date.accessioned | 2024-04-15T09:45:43Z | |
| dc.date.available | 2024-04-15T09:45:43Z | |
| dc.date.created | 2011-02-25 | |
| dc.date.issued | 2011 | |
| dc.date.conference | 2011 | |
| dc.identifier.uri | https://oskar-bordeaux.fr/handle/20.500.12278/197944 | |
| dc.description.abstractEn | 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. | |
| dc.description.sponsorship | Frontières de la reconnaissabilité - ANR-10-BLAN-0202 | |
| dc.language.iso | en | |
| dc.source.title | Krivine Machines and Higher-Order Schemes | |
| dc.type | Communication dans un congrès | |
| dc.subject.hal | Informatique [cs]/Logique en informatique [cs.LO] | |
| bordeaux.page | 162-173 | |
| bordeaux.volume | 6756 | |
| bordeaux.hal.laboratories | Laboratoire Bordelais de Recherche en Informatique (LaBRI) - UMR 5800 | * |
| bordeaux.institution | Université de Bordeaux | |
| bordeaux.institution | Bordeaux INP | |
| bordeaux.institution | CNRS | |
| bordeaux.conference.title | ICALP | |
| bordeaux.country | CH | |
| bordeaux.title.proceeding | Krivine Machines and Higher-Order Schemes | |
| bordeaux.peerReviewed | oui | |
| hal.identifier | hal-00570017 | |
| hal.version | 1 | |
| hal.invited | non | |
| hal.proceedings | oui | |
| hal.popular | non | |
| hal.audience | Non spécifiée | |
| dc.title.de | Krivine machines and higher-order schemes | |
| hal.origin.link | https://hal.archives-ouvertes.fr//hal-00570017v1 | |
| bordeaux.COinS | ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.btitle=Krivine%20Machines%20and%20Higher-Order%20Schemes&rft.date=2011&rft.volume=6756&rft.spage=162-173&rft.epage=162-173&rft.au=SALVATI,%20Sylvain&WALUKIEWICZ,%20Igor&rft.genre=unknown |
Fichier(s) constituant ce document
| Fichiers | Taille | Format | Vue |
|---|---|---|---|
|
Il n'y a pas de fichiers associés à ce document. |
|||