Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/hal-03545768
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

File

RR-9475.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03545768, version 2

Citation

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

Share

Metrics

Record views

81

Files downloads

54