Non-Deterministic Abstract Machines - Université de Lorraine Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2022

Non-Deterministic Abstract Machines

Résumé

We present a generic design of abstract machines for nondeterministic programming languages, such as process calculi or concurrent lambda calculi, that provides a simple way to implement them. Such a machine traverses a term in the search for a redex, making non-deterministic choices when several paths are possible and backtracking when it reaches a dead end, i.e., an irreducible subterm. The search is guaranteed to terminate thanks to term annotations the machine introduces along the way. We show how to automatically derive a non-deterministic abstract machine from a zipper semantics-a form of structural operational semantics in which the decomposition process of a term into a context and a redex is made explicit. The derivation method ensures the soundness and completeness of the machines w.r.t. the zipper semantics.
Fichier principal
Vignette du fichier
lics.pdf (652.71 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03545768 , version 1 (27-01-2022)
hal-03545768 , version 2 (01-07-2022)

Identifiants

  • HAL Id : hal-03545768 , version 1

Citer

Małgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, Alan Schmitt. Non-Deterministic Abstract Machines. 2022. ⟨hal-03545768v1⟩
240 Consultations
154 Téléchargements

Partager

Gmail Facebook X LinkedIn More