2026-07-22T14:20:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17070 2024-03-06T10:58:40Z ddc:004 open_access

Non-Deterministic Abstract Machines Biernacka, Małgorzata Biernacki, Dariusz Lenglet, Sergueï Schmitt, Alan Abstract machines non-determinism lambda-calculus process calculi We present a generic design of abstract machines for non-deterministic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Małgorzata Biernacka and Dariusz Biernacki and Sergueï Lenglet and Alan Schmitt 2022 Is Part Of LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2022.7 urn:nbn:de:0030-drops-170705 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.7 eng https://creativecommons.org/licenses/by/4.0/legalcode