Skip to main content

Questions tagged [operational-semantics]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
0 answers
57 views

Are there any programming languages based on the method of analytic tableaux, aside from Fitting's Proflog?

The method of analytic tableaux [0] describes a process by which logical formulae, particularly of first order logic, can be determined to be valid or invalid. From the Wikipedia entry: A tableau ...
jpt4's user avatar
  • 111
2 votes
1 answer
206 views

Operational semantics and denotational semantics and describing the behaviour and structure of programs

I was under the impression that operational semantics describes the behaviour of a program (so it includes the implementation details / the implementation matters), whereas denotational semantics ...
The Pointer's user avatar
4 votes
3 answers
152 views

Formalization of matching logic (logic behind K Framework)

Is there any mechanization for matching logic (any flavor)? I only find study about K Framework rules to Deducti translation, but this is both not covering to matching logic and not internalizing the ...
uhbif19's user avatar
  • 315
9 votes
1 answer
170 views

What's the relation between applicative bisimulation and context equivalence in the $\lambda$-calculus?

I've seem two different notions of operational equivalence being used for the $\lambda$-lalculus, i.e., an equivalence stating that "if we replace term $a$ with a term $b$ in a program, the ...
paulotorrens's user avatar
-1 votes
1 answer
111 views

Why structural rules define the "smallest relation" satisfying the rules? [closed]

I'm following a university course based on these slides, and I have a question about structural operational semantics. As you can see at page 7 (4-th slide), a structural rule is interpreted logically ...
user402843's user avatar
4 votes
0 answers
135 views

Origin of simulation relations for compiler correctness

Leroy uses simulation relations as a means of showing compiler correctness; the basic idea is that a simulation relation is an asymmetric binary relation between states in two different small step ...
denotational's user avatar
1 vote
0 answers
65 views

Effect handlers, arrows and applicatives

After reading Lindley's paper on effect handlers for arrows and applicatives, I got the gist about dynamic and static flow and that it was added to the effect system and so on. However, I do not ...
Jesper Dahl's user avatar
3 votes
2 answers
332 views

Moggi's computational metalanguage

In Notions of Computation and Monads Moggi models the notion of a computation of type $A$, $TA$, using a monad $T$. Among other things this ensures the $T\eta$ rule: $$\frac{x: A \vdash a:TB}{x:A \...
Andrew Bacon's user avatar
7 votes
1 answer
372 views

Do we care about confluence because of unique normal forms?

Confluence implies uniqueness of normal forms, which is great. It is also much simpler to reason about, allowing more reusable proofs (indeed I don't imagine a way to prove UN directly for the $\...
Guido's user avatar
  • 181
1 vote
0 answers
131 views

Has there been work on formal Semantics for linear algebra?

Could I get some references on formal semantics for a calculus on linear algebra that helps you study matrix or tensor based programming languages? I am looking for anything that encompasses linear or ...
ArtisanV's user avatar
  • 119
3 votes
1 answer
172 views

What is contextual equivalence ignoring non-termination called?

Contextual equivalence ($M_1 \cong_{ctx} M_2$) is often defined as: $C[M_1] \Downarrow V \iff C[M_2] \Downarrow V$ Which is to say for any context $C$, $C[M_1]$ terminates with value $V$ iff $C[M_2]$...
Will's user avatar
  • 133
13 votes
3 answers
906 views

For what languages is there already a theory of observational equivalence?

For a correctness proof, I'm looking for a usable notion of program equivalence $\cong$ for Barendregt's pure type systems (PTSs); missing that, for enough specific type systems. My goal is simply to ...
Blaisorblade's user avatar
  • 2,069
1 vote
1 answer
175 views

Name a set of program variables

I am interested in the set of the variables that satisfy the following properties. I would like to find a proper name for them. We assume that a program $\phi$ has a set of variables $v_0, \ldots, ...
SoftTimur's user avatar
16 votes
1 answer
641 views

Can we distinguish strictly syntactic and semantic methods in programming language?

While discussion strong normalization proofs, this comment contrasts the "normal forms model" with "purely syntactic methods". This brings me back to a more basic question: can we still distinguish ...
Blaisorblade's user avatar
  • 2,069
2 votes
2 answers
310 views

Tool for specifying operational semantics for given formally specified programming language

I am trying to translate code from one programming language into another (to be specific - from RuleML to Drools, but other pairs can be expected as well) and it would be nice to know - whether there ...
TomR's user avatar
  • 409
2 votes
0 answers
204 views

Evaluation contexts: outside-in vs inside-out

I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
day's user avatar
  • 2,805
0 votes
1 answer
136 views

How would you define a set of 'fundamental operations' over an object? [closed]

I'm writing an implementation for a common array structure. As you would find already familiar, an array is an ordered data structure that you can transform with different (hopefully self-explained) ...
Alex Morales's user avatar
8 votes
1 answer
632 views

Step-indexing: Where to begin?

I am about to begin a verification project (for MIPS) with my professor (I am a senior undergraduate) and have been told that the soundness proof for the program logic we need will probably involve ...
C.E.Sally's user avatar
  • 313
0 votes
0 answers
92 views

Semantics of a programming language [duplicate]

A newbie question, if I may... Could you be so kind and explain to me in plain english meaning of 'denotational semantics' and 'operational semantics'? I'm familiar with the definitions and have read ...
svetlana's user avatar
  • 101
13 votes
1 answer
2k views

Can Scheme's call/cc implement all known control flow structures?

The page "Advanced Scheme: Some Naughty Bits" states: Continuations are a powerful control-flow construct from which nearly any other control-flow structure [...] may be derived. I thought that ...
csl's user avatar
  • 133
10 votes
1 answer
2k views

What is the difference between meaning and denotation?

In programming language semantics, it is often heard that people talking about meaning and denotation. They seem not to be the same. What is the difference? Is the former associated with ...
day's user avatar
  • 2,805
5 votes
1 answer
273 views

Characterizing closure under expansion/reduction for big-step semantics?

Two common ways of formulating operational semantics for programming languages based on lambda-calculus are big-step and small-step semantics. In a big step semantics, you give a relation $e \...
Neel Krishnaswami's user avatar