Afficher la notice abrégée

Krivine machines and higher-order schemes

hal.structure.identifierLinguistic signs, grammar and meaning: computational logic for natural language [SIGNES]
hal.structure.identifierLaboratoire Bordelais de Recherche en Informatique [LaBRI]
dc.contributor.authorSALVATI, Sylvain
hal.structure.identifierLaboratoire Bordelais de Recherche en Informatique [LaBRI]
dc.contributor.authorWALUKIEWICZ, Igor
dc.date.accessioned2024-04-15T09:47:31Z
dc.date.available2024-04-15T09:47:31Z
dc.date.issued2011
dc.identifier.urihttps://oskar-bordeaux.fr/handle/20.500.12278/198102
dc.description.abstractEnWe 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.language.isoen
dc.typeRapport
dc.subject.halInformatique [cs]/Logique en informatique [cs.LO]
bordeaux.page17
bordeaux.hal.laboratoriesLaboratoire Bordelais de Recherche en Informatique (LaBRI) - UMR 5800*
bordeaux.institutionUniversité de Bordeaux
bordeaux.institutionBordeaux INP
bordeaux.institutionCNRS
bordeaux.type.reportrr
hal.identifierinria-00589407
hal.version1
hal.audienceNon spécifiée
dc.title.deKrivine machines and higher-order schemes
hal.origin.linkhttps://hal.archives-ouvertes.fr//inria-00589407v1
bordeaux.COinSctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.date=2011&rft.spage=17&rft.epage=17&rft.au=SALVATI,%20Sylvain&WALUKIEWICZ,%20Igor&rft.genre=unknown


Fichier(s) constituant ce document

FichiersTailleFormatVue

Il n'y a pas de fichiers associés à ce document.

Ce document figure dans la(les) collection(s) suivante(s)

Afficher la notice abrégée