# Questions tagged [operational-semantics]

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms.

12 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
0answers
160 views

### Is there relation between K-Framework and structural operational semantics?

K-framework strives to give one (instead of two - operational and denotational) semantics for industrial programming languages. The same unification is done by structural operational semantic as well. ...
0answers
390 views

### How are observational equivalence, contextual equivalence, and extensional equality related?

First, some context: I'm reading this blog post by Andrej Bauer. So, I stumbled in these terms: "observational equivalence" and "contextual equivalence". I know almost nothing about operational ...
0answers
559 views

### How to decide between operational, denotational, and axiomatic semantics?

Context I'm designing a language which implements lambda calculus and (first-order) predicate calculus, where lambdas behave as the abstraction encapsulating logic, compositionally forming a ...
0answers
50 views

### Termination of deterministic term rewriting

Consider a simple language: $$t ::= plus ~ t ~ t ~ | ~ gen ~ t ~ | ~ except ~ N ~ t ~ | ~ N$$ with N constructors plus, gen and except, N being the natural numbers, and $G = \{t_n\}$ a finite, ...
0answers
25 views

### structural operational semantic equivalence

We add the following derivation rule to the structural operational semantic: < repeat S until b, s >$\Rightarrow$ < S; if b then skip else (repeat S until b) > Prove that "repeat S until b" is ...
0answers
113 views

### Small step vs big step semantics for static analysis?

To be an honest question poster I do not yet fully grasp the difference between small step and big step semantics. There was a good discussion here My question is if I were to do static analysis on ...
0answers
62 views

### Operational Semantics - Include SKIP, SEQUENCE and IF?

I'm writing a paper for a programming languages workshop in which I have to describe the semantics of a new optimization for Java using Operational Semantics, small step style. I have never used ...
0answers
130 views

### Program equivalence with Structural induction

I recently attended my first lecture on structural induction and the professor stated that structural induction can be used to to prove that two programming languages are equivalent. I am new to ...
0answers
70 views

### Why algebraic semantics of programming languages have died out and have not used today?

Algebraic semantics is one type of semantics that uses algebraic expressions for connecting the formal descriptions of initial and final states of some operation of some operation that is defined in ...
0answers
102 views

### Reasonable definition of beta-equivalence in big-step semantics

Assume, an extension of the lambda calculus with terms $t$ and values $v$ is defined in big-step operational semantics with evaluation relation $t \Downarrow v$. It is intuitive to assume that $\beta$...
0answers
41 views

### How to check if two program are simulated or bisimulated?

Suppose I have programs A and B defined in this way: ...
0answers
172 views

### Proving the small-step semantics of factorial program

I am given the following command $C$: $y:=1;$ while $\neg (x=1)$ do $y:= y*x;$ $x:= x - 1$. I have to show that $[\![ C ]\!]_s(s) = \{x \mapsto 1, y \mapsto s(x)!\}$ if $s(x) \geq 1$ and undefined ...