We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Soundness conditions for big-step semantics

Formale Metadaten

Titel
Soundness conditions for big-step semantics
Serientitel
Anzahl der Teile
13
Autor
Mitwirkende
Lizenz
CC-Namensnennung 3.0 Deutschland:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr2021
SpracheEnglisch

Inhaltliche Metadaten

Fachgebiet
Genre
Abstract
We propose a general proof technique to show that a predicate is \emph{sound}, that is, prevents stuck computation, with respect to a big-step semantics. This result may look surprising, since in big-step semantics there is no difference between non-terminating and stuck computations, hence soundness cannot even be expressed. The key idea is to define constructions yielding an extended version of a given arbitrary big-step semantics, where the difference is made explicit. The extended semantics are exploited in the meta-theory, notably they are necessary to show that the proof technique works. However, they remain transparent when using the proof technique, since it consists in checking three conditions on the original rules only, as we illustrate by several examples.
Schlagwörter