Concepts and Semantics of Programming Languages 1 - Francois Pessaux

. .

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...

Biographie:

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 Exp₂ 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 Exp₂ 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 Exp₂ 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

5.5.2. Properties of the inference algorithm 167