Omnisemantics: Smoother Handling of Nondeterminism - Inserm - Institut national de la santé et de la recherche médicale Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2022

Omnisemantics: Smoother Handling of Nondeterminism

Résumé

This paper gives an in-depth presentation of the omni-big-step and omni-small-step styles of semantic judgments. These styles describe operational semantics by relating starting states to sets of outcomes rather than to individual outcomes. A single derivation of these semantics for a particular starting state and program describes all possible nondeterministic executions (hence the name "omni"), whereas in traditional small-step and big-step semantics, each derivation only talks about one single execution. This restructuring allows for straightforward modeling of languages featuring both nondeterminism and undefined behavior. Specifically, omnisemantics inherently assert safety, i.e. they guarantee that none of the execution branches gets stuck, while traditional semantics need either a separate judgment or additional error markers to specify safety in the presence of nondeterminism. Omnisemantics can be understood as an inductively defined weakest-precondition semantics (or more generally, predicate-transformer semantics) that does not involve invariants for loops and recursion, but instead uses unrolling rules like in traditional small-step and big-step semantics. Omnisemantics have already been used in the past, but we believe that it has been under-appreciated and that it deserves a well-motivated, extensive and pedagogical presentation of its benefits. We also explore several novel aspects associated with these semantics, in particular their use in type-soundness proofs for lambda calculi, partial-correctness reasoning, and forward proofs of compiler correctness for terminating but potentially nondeterministic programs being compiled to nondeterministic target languages.
Fichier principal
Vignette du fichier
omnisemantics.pdf (730.69 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03255472 , version 1 (09-06-2021)
hal-03255472 , version 2 (17-03-2022)
hal-03255472 , version 3 (28-09-2022)

Identifiants

  • HAL Id : hal-03255472 , version 2

Citer

Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter. Omnisemantics: Smoother Handling of Nondeterminism. 2022. ⟨hal-03255472v2⟩
521 Consultations
397 Téléchargements

Partager

Gmail Facebook X LinkedIn More