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

Formal Metadata

Title
Soundness conditions for big-step semantics
Title of Series
Number of Parts
13
Author
Contributors
License
CC Attribution 3.0 Germany:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date2021
LanguageEnglish

Content Metadata

Subject Area
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.
Keywords