Concepts and Semantics of Programming Languages 1

This book the first of two volumes explores the syntactical constructs
of the most common programming languages, and sheds a
mathematical light on their semantics, while also providing an accurate
presentation of the material aspects that interfere with coding.

Concepts and Semantics of Programming Languages 1 is dedicated to
functional and imperative features. Included is the formal study of the
semantics of typing and execution; their acquisition is facilitated by
implementation into OCaml and Python, as well as by worked examples.
Data representation is considered in detail: endianness, pointers,
memory management, union types and pattern-matching, etc., with
examples in OCaml, C and C++. The second volume introduces a specific
model for studying modular and object features and uses this model to
present Ada and OCaml modules, and subsequently Java, C++, OCaml
and Python classes and objects.

This book is intended not only for computer science students and
teachers but also seasoned programmers, who will find a guide to
reading reference manuals and the foundations of program verification.

Auteur

Therese Hardin is Professor Emeritus at the Laboratoire d?Informatique de Paris 6 (LIP6), Sorbonne University, France. Mathieu Jaume is a lecturer at the Laboratoire d?Informatique de Paris 6 (LIP6), Sorbonne University, France. Francois Pessaux is Associate Professor in the Computer Science and Systems Engineering Unit (U2IS) of ENSTA Paris, France. Veronique Viguie Donzeau-Gouge is Professor Emeritus at the Centre d?etudes et de recherche en informatique (CEDRIC) of the Conservatoire national des arts et metiers (Cnam Paris), France.

Texte du rabat
This book the first of two volumes explores the syntactical constructsof the most common programming languages, and sheds amathematical light on their semantics, while also providing an accuratepresentation of the material aspects that interfere with coding.

Concepts and Semantics of Programming Languages 1 is dedicated tofunctional and imperative features. Included is the formal study of thesemantics of typing and execution; their acquisition is facilitated byimplementation into OCaml and Python, as well as by worked examples.Data representation is considered in detail: endianness, pointers,memory management, union types and pattern-matching, etc., withexamples in OCaml, C and C++. The second volume introduces a specificmodel for studying modular and object features and uses this model topresent Ada and OCaml modules, and subsequently Java, C++, OCamland Python classes and objects.

This book is intended not only for computer science students andteachers but also seasoned programmers, who will find a guide toreading reference manuals and the foundations of program verification.

Résumé
This book the first of two volumes explores the syntactical constructs of the most common programming languages, and sheds a mathematical light on their semantics, while also providing an accurate presentation of the material aspects that interfere with coding. Concepts and Semantics of Programming Languages 1 is dedicated to functional and imperative features. Included is the formal study of the semantics of typing and execution; their acquisition is facilitated by implementation into OCaml and Python, as well as by worked examples. Data representation is considered in detail: endianness, pointers, memory management, union types and pattern-matching, etc., with examples in OCaml, C and C++. The second volume introduces a specific model for studying modular and object features and uses this model to present Ada and OCaml modules, and subsequently Java, C++, OCaml and Python classes and objects. This book is intended not only for computer science students and teachers but also seasoned programmers, who will find a guide to reading reference manuals and the foundations of program verification.

Contenu
Foreword xi

Preface xiii

Chapter 1. From Hardware to Software 1

1.1. Computers: a low-level view 1

1.1.1. Information processing 1

1.1.2. Memories 2

1.1.3. CPUs 3

1.1.4. Peripheral devices 7

1.2. Computers: a high-level view 8

1.2.1. Modeling computations 9

1.2.2. High-level languages 9

1.2.3. From source code to executable programs 10

Chapter 2. Introduction to Semantics of Programming Languages 15

2.1. Environment, memory and state 16

2.1.1. Evaluation environment 16

2.1.2. Memory 18

2.1.3. State 20

2.2. Evaluation of expressions 21

2.2.1. Syntax 21

2.2.2. Values 22

2.2.3. Evaluation semantics 24

2.3. Definition and assignment 26

2.3.1. Defining an identifier 26

2.3.2. Assignment 29

2.4. Exercises 31

Chapter 3. Semantics of Functional Features 35

3.1. Syntactic aspects 35

3.1.1. Syntax of a functional kernel 35

3.1.2. Abstract syntax tree 36

3.1.3. Reasoning by induction over expressions 39

3.1.4. Declaration of variables, bound and free variables 39

3.2. Execution semantics: evaluation functions 42

3.2.1. Evaluation errors 42

3.2.2. Values 43

3.2.3. Interpretation of operators 45

3.2.4. Closures 46

3.2.5. Evaluation of expressions 47

3.3. Execution semantics: operational semantics 54

3.3.1. Simple expressions 55

3.3.2. Call-by-value 56

3.3.3. Recursive and mutually recursive functions 60

3.3.4. Call-by-name 61

3.3.5. Call-by-value versus call-by-name 62

3.4. Evaluation functions versus evaluation relations 64

3.4.1. Status of the evaluation function 64

3.4.2. Induction over evaluation trees 65

3.5. Semantic properties 69

3.5.1. Equivalent expressions 69

3.5.2. Equivalent environments 71

3.6. Exercises 71

Chapter 4. Semantics of Imperative Features 77

4.1. Syntax of a kernel of an imperative language 77

4.2. Evaluation of expressions 81

4.3. Evaluation of definitions 86

4.4. Operational semantics 89

4.4.1. Big-step semantics 89

4.4.2. Small-step semantics 93

4.4.3. Expressiveness of operational semantics 95

4.5. Semantic properties 96

4.5.1. Equivalent programs 96

4.5.2. Program termination 98

4.5.3. Determinism of program execution 100

4.5.4. Big steps versus small steps 103

4.6. Procedures 109

4.6.1. Blocks 109

4.6.2. Procedures 112

4.7. Other approaches 118

4.7.1. Denotational semantics 118

4.7.2. Axiomatic semantics, Hoare logic 129

4.8. Exercises 134

Chapter 5. Types 137

5.1. Type checking: when and how? 139

5.1.1. When to verify types? 139

5.1.2. How to verify types? 140

5.2. Informal typing of a program Exp2 141

5.2.1. A first example 141

5.2.2. Typing a conditional expression 142

5.2.3. Typing without type constraints 142

5.2.4. Polymorphism 143

5.3. Typing rules in Exp2 143

5.3.1. Types, type schemes and typing environments 143

5.3.2. Generalization, substitution and instantiation 146

5.3.3. Typing rules and typing trees 151

5.4. Type inference algorithm in Exp2 154

5.4.1. Principal type 154

5.4.2. Sets of constraints and unification 155

5.4.3. Type inference algorithm 159

5.5. Properties 167 5.5.1. Properties of typechecking 167</p...