Programming Languages and Operational Semantics: A Concise Overview (Undergraduate Topics in Computer Science)
Format: PDF / Kindle (mobi) / ePub
This concise introduction to the essential concepts in contemporary programming languages features a host of illustrative examples. It explains modern imperative, functional, and logic-based languages as well as giving readers the tools to design new ones.
included; these are marked with . Answers to selected exercises are given in the final chapter of the book. The book is organised as follows: Part I provides an introduction to programming languages and operational semantics in Chap. 1 , followed by basic mathematical background for the rest of the book in Chap. 2 . In Part II we study the main components of imperative languages. We first give an informal description in Chap. 3 , and then give a formal specification of the main constructs
location in . We write to denote the function that maps each to the value , and to the value (so the function coincides with everywhere except in , where they may differ). Formally, an abstract machine is a transition system, and is therefore defined by a set of configurations and a transition relation (see Sect. 2.3 in Chap. 2). The transition relation will be defined by transition rules. Configurations. The configurations of the abstract machine for SIMP are triples of control stack,
Haskell as , where is the type of the elements of the list; for instance, [Integer] is the type of lists of integers. Strings are lists of characters, such as “Hello”. Function types: , are all examples of function types, or arrow types. By convention, arrows associate to the right, that is, should be read as This is the type of a higher-order function that takes an integer and produces a function from integers to integers as a result. In functional languages, functions can be used as
program is correctly typed in the environment if for each equation in , where , we have In other words, a FUN program is well-typed if the equations are compatible with the types declared by the programmer for the global functions. The term in the right hand side of the th equation should have the type of , that is, . Note that may be 0. In contrast with SFUN, here may be any type, for instance it could be an arrow type if the result of is a function. To type the term we use the type system
similarities with the approach used in natural sciences to explain natural processes, where a mathematical model of the system under study is built, then natural processes are explained in terms of the model. In the case of programming languages, the model deals with computation, and it should be sufficiently powerful to allow us to explain the meaning of all the constructs in the language. Axiomatic: The meaning of programs is given by describing the properties that hold before and after the