scholarly journals The semantics of programming languages: An elementary introduction using structural operational semantics

1991 ◽  
Vol 16 (3) ◽  
pp. 278-279
Author(s):  
Ian J. Hayes
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Semantics Of Programming Languages ◽  
Structural Operational Semantics

scholarly journals Structural Operational Semantics

1999 ◽  
Vol 6 (30) ◽  
Author(s):  
Luca Aceto ◽  
Willem Jan Fokkink ◽  
Chris Verhoef
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
The Sixties ◽  
Structural Operational Semantics ◽  
High Level

The importance of giving precise semantics to programming and specification<br />languages was recognized since the sixties with the development of the<br />first high-level programming languages (cf. e.g. [30, 206] for some early accounts).<br />The use of operational semantics - i.e. of a semantics that explicitly<br />describes how programs compute in stepwise fashion, and the possible<br />state-transformations they perform - was already advocated by McCarthy<br />in [147], and elaborated upon in references like [142, 143]. Examples of full-blown<br />languages that have been endowed with an operational semantics are<br />Algol 60 [140], PL/I [173], and CSP [178].

scholarly journals Denotational semantics of recursive types in synthetic guarded domain theory

2018 ◽  
Vol 29 (3) ◽  
pp. 465-510 ◽  
Author(s):  
RASMUS E. MØGELBERG ◽  
MARCO PAVIOTTI
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Denotational Semantics ◽  
Domain Theory ◽  
Logical Relation ◽  
Dependent Type Theory ◽  
Semantics Of Programming Languages ◽  
Dependent Type

Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.Working inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally, we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

scholarly journals Categorical model of structural operational semantics for imperative language

2016 ◽  
Vol 40 (2) ◽  
pp. 203-219 ◽  
Author(s):  
William Steingartner ◽  
Valerie Novitzká
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Mathematical Structure ◽  
Program Behavior ◽  
Elementary Steps ◽  
Categorical Model ◽  
Structural Operational Semantics ◽  
State Changes ◽  
Definition Of ◽  
Graphical Illustration

Definition of programming languages consists of the formal definition of syntax and semantics. One of the most popular semantic methods used in various stages of software engineering is structural operational semantics. It describes program behavior in the form of state changes after execution of elementary steps of program. This feature makes structural operational semantics useful for implementation of programming languages and also for verification purposes. In our paper we present a new approach to structural operational semantics. We model behavior of programs in category of states, where objects are states, an abstraction of computer memory and morphisms model state changes, execution of a program in elementary steps. The advantage of using categorical model is its exact mathematical structure with many useful proved properties and its graphical illustration of program behavior as a path, i.e. a composition of morphisms. Our approach is able to accentuate dynamics of structural operational semantics. For simplicity, we assume that data are intuitively typed. Visualization and facility of our model is not only a new model of structural operational semantics of imperative programming languages but it can also serve for education purposes.

scholarly journals A Modular SOS for Action Notation

1999 ◽  
Vol 6 (56) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Specification Language ◽  
Algebraic Specification ◽  
Recent Proposal ◽  
Structural Operational Semantics ◽  
The Common ◽  
Basic Concepts ◽  
Pragmatic Aspect

Modularity is an important pragmatic aspect of semantic<br />descriptions: good modularity is needed to allow the reuse of existing descriptions when extending or changing the described language. In denotational semantics, the issue of modularity has received much attention, and appropriate abstractions have been introduced, so that definitions of semantic functions may be independent of the details of how computations are modeled. In structural operational semantics (SOS), however, this issue has largely been neglected, and SOS descriptions of programming languages typically exhibit rather poor modularity; the original SOS given for Action Notation (the notation for the semantic entities used in action semantics) suffered from the same problem.<br />This paper recalls a recent proposal, called MSOS, for obtaining a high<br />degree of modularity in SOS, and presents an MSOS description of Action<br />Notation. Due to its modularity, the MSOS description pinpoints some<br />complications in the design of Action Notation, and should facilitate the<br />design of an improved version of the notation. It also provides a major<br />example of the applicability of the MSOS framework.<br />The reader is assumed to be familiar with conventional SOS and with<br />the basic concepts and constructs of Action Notation. The description<br />of Action Notation is formulated almost entirely in Casl, the common<br />algebraic specification language.

scholarly journals From CML to process Algebras

1993 ◽  
Vol 22 (433) ◽  
Author(s):  
Flemming Nielson ◽  
Hanne Riis Nielson
Keyword(s):  
Programming Languages ◽  
Programming Language ◽  
Process Algebra ◽  
Operational Semantics ◽  
Concurrent Programming ◽  
Process Algebras ◽  
Standard Ml ◽  
Concurrent Programming Languages ◽  
Structural Operational Semantics ◽  
Communication Behaviours

<p>Reppy's language CML extends Standard ML of Milner et al. with primitives for communication. It thus inherits a notion of strong polymorphic typing and may be equipped with a structural operational semantics. We formulate an effect system for statically expressing the communication behaviours of CML programs as these are not otherwise reflected in the types.</p><p>We then show how types and behaviours evolve in the course of computation: types may decrease and behaviours may loose alternatives as well as decrease. It will turn out that the syntax of behaviours is rather similar to that of a process algebra; our main results may therefore be viewed as regarding the semantics of a process algebra as an <em>abstraction</em> of the semantics of an underlying programming language. This establishes a new kind of connection between ''realistic'' concurrent programming languages and ''theoretical'' process algebras.</p>

scholarly journals Exploiting Labels in Structural Operational Semantics

2005 ◽  
Vol 12 (8) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Concurrent Systems ◽  
Sequential Programming ◽  
Structural Operational Semantics ◽  
Full Power

Structural Operational Semantics (SOS) allows transitions to be labelled. This is fully exploited in SOS descriptions of concurrent systems, but usually not at all in conventional descriptions of sequential programming languages.<br /> <br />This paper shows how the use of labels can provide significantly simpler and more modular descriptions of programming languages. However, the full power of labels is obtained only when the set of labels is made into a category, as in the recently-proposed MSOS variant of SOS.

scholarly journals Logical Specification of Operational Semantics

1999 ◽  
Vol 6 (55) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Programming Languages ◽  
Operational Semantics ◽  
Rewriting Logic ◽  
Horn Logic ◽  
Semantics Of Programming Languages ◽  
Crucial Feature ◽  
Logical Specification ◽  
Inference Systems ◽  
Equational Specifications ◽  
The Relationship

Various logic-based frameworks have been proposed for <br />specifying the operational semantics of programming languages and <br />concurrent systems, including inference systems in the styles advocated by<br />Plotkin and by Kahn, Horn logic, equational specifications, reduction<br />systems for evaluation contexts, rewriting logic, and tile logic.<br />We consider the relationship between these frameworks, and assess their<br />respective merits and drawbacks - especially with regard to the modularity<br /> of specifications, which is a crucial feature for scaling up to practical<br />applications. We also report on recent work towards the use of the Maude<br />system (which provides an efficient implementation of rewriting logic) as<br />a meta-tool for operational semantics.

Sign in / Sign up

Export Citation Format

Share Document