Skip to Main content Skip to Navigation

Non-Deterministic Abstract Machines

Małgorzata Biernacka 1 Dariusz Biernacki 1 Serguei Lenglet 2, 3 Alan Schmitt 4 
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : 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.
Complete list of metadata
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Friday, July 1, 2022 - 2:52:40 PM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM


Files produced by the author(s)


  • HAL Id : hal-03545768, version 2


Małgorzata Biernacka, Dariusz Biernacki, Serguei Lenglet, Alan Schmitt. Non-Deterministic Abstract Machines. [Research Report] RR-9475, Inria. 2022, pp.33. ⟨hal-03545768v2⟩



Record views


Files downloads