Concepts and Semantics of Programming Languages 1: A Semantical Approach with OCaml and Python

Cover
Half-Title Page
Title Page
Copyright Page
Contents
Foreword
Preface
1 From Hardware to Software
	1.1. Computers: a low-level view
		1.1.1. Information processing
		1.1.2. Memories
		1.1.3. CPUs
		1.1.4. Peripheral devices
	1.2. Computers: a high-level view
		1.2.1. Modeling computations
		1.2.2. High-level languages
		1.2.3. From source code to executable programs
2 Introduction to Semantics of Programming Languages
	2.1. Environment, memory and state
		2.1.1. Evaluation environment
		2.1.2. Memory
		2.1.3. State
	2.2. Evaluation of expressions
		2.2.1. Syntax
		2.2.2. Values
		2.2.3. Evaluation semantics
	2.3. Definition and assignment
		2.3.1. Defining an identifier
		2.3.2. Assignment
	2.4. Exercises
		Exercise 2.1
		Exercise 2.2
3 Semantics of Functional Features
	3.1. Syntactic aspects
		3.1.1. Syntax of a functional kernel
		3.1.2. Abstract syntax tree
		3.1.3. Reasoning by induction over expressions
		3.1.4. Declaration of variables, bound and free variables
	3.2. Execution semantics: evaluation functions
		3.2.1. Evaluation errors
		3.2.2. Values
		3.2.3. Interpretation of operators
		3.2.4. Closures
		3.2.5. Evaluation of expressions
	3.3. Execution semantics: operational semantics
		3.3.1. Simple expressions
		3.3.2. Call-by-value
		3.3.3. Recursive and mutually recursive functions
		3.3.4. Call-by-name
		3.3.5. Call-by-value versus call-by-name
	3.4. Evaluation functions versus evaluation relations
		3.4.1. Status of the evaluation function
		3.4.2. Induction over evaluation trees
	3.5. Semantic properties
		3.5.1. Equivalent expressions
		3.5.2. Equivalent environments
	3.6. Exercises
		Exercise 3.1
		Exercise 3.2
		Exercise 3.3
		Exercise 3.4
		Exercise 3.5
		Exercise 3.6
		Exercise 3.7
4 Semantics of Imperative Features
	4.1. Syntax of a kernel of an imperative language
	4.2. Evaluation of expressions
	4.3. Evaluation of definitions
	4.4. Operational semantics
		4.4.1. Big-step semantics
		4.4.2. Small-step semantics
		4.4.3. Expressiveness of operational semantics
	4.5. Semantic properties
		4.5.1. Equivalent programs
		4.5.2. Program termination
		4.5.3. Determinism of program execution
		4.5.4. Big steps versus small steps
	4.6. Procedures
		4.6.1. Blocks
		4.6.2. Procedures
	4.7. Other approaches
		4.7.1. Denotational semantics
		4.7.2. Axiomatic semantics, Hoare logic
	4.8. Exercises
		Exercise 4.1
		Exercise 4.2
		Exercise 4.3
5 Types
	5.1. Type checking: when and how?
	5.1.1. When to verify types?
	5.1.2. How to verify types?
	5.2. Informal typing of a program Exp2
		5.2.1. A first example
		5.2.2. Typing a conditional expression
		5.2.3. Typing without type constraints
		5.2.4. Polymorphism
	5.3. Typing rules in Exp2
		5.3.1. Types, type schemes and typing environments
		5.3.2. Generalization, substitution and instantiation
		5.3.3. Typing rules and typing trees
	5.4. Type inference algorithm in Exp2
		5.4.1. Principal type
		5.4.2. Sets of constraints and unification
		5.4.3. Type inference algorithm
	5.5. Properties
		5.5.1. Properties of typechecking
		5.5.2. Properties of the inference algorithm
	5.6. Typechecking of imperative constructs
		5.6.1. Type algebra
		5.6.2. Typing rules
		5.6.3. Typing polymorphic definitions
	5.7. Subtyping and overloading
		5.7.1. Subtyping
		5.7.2. Overloading
6 Data Types
	6.1. Basic types
		6.1.1. Booleans
		6.1.2. Integers
		6.1.3. Characters
		6.1.4. Floating point numbers
	6.2. Arrays
	6.3. Strings
	6.4. Type definitions
		6.4.1. Type abbreviations
		6.4.2. Records
		6.4.3. Enumerated types
		6.4.4. Sum types
	6.5. Generalized conditional
		6.5.1. C style switch/case
		6.5.2. Pattern matching
	6.6. Equality
		6.6.1. Physical equality
		6.6.2. Structural equality
		6.6.3. Equality between functions
7 Pointers and Memory Management
	7.1. Addresses and pointers
	7.2. Endianness
	7.3. Pointers and arrays
	7.4. Passing parameters by address
	7.5. References
		7.5.1. References in C++
		7.5.2. References in Java
	7.6. Memory management
		7.6.1. Memory allocation
		7.6.2. Freeing memory
		7.6.3. Automatic memory management
8 Exceptions
	8.1. Errors: notification and propagation
		8.1.1. Global variable
		8.1.2. Record definition
		8.1.3. Passing by address
		8.1.4. Introducing exceptions
	8.2. A simple formalization: ML-style exceptions
		8.2.1. Abstract syntax
		8.2.2. Values
		8.2.3. Type algebra
		8.2.4. Operational semantics
		8.2.5. Typing
	8.3. Exceptions in other languages
		8.3.1. Exceptions in OCaml
		8.3.2. Exceptions in Python
		8.3.3. Exceptions in Java
		8.3.4. Exceptions in C++
Conclusion
Solutions to the Exercises
	A.1. Introduction to language semantics Solution to exercise 2.1
	Solution to exercise 2.2
	A.2. Semantics of functional features Solution to exercise 3.1
	Solution to exercise 3.2
	Solution to exercise 3.3
	Solution to exercise 3.4
	Solution to exercise 3.5
	Solution to exercise 3.6
	Solution to exercise 3.7
	A.3. Semantics of imperative features Solution to exercise 4.1
	Solution to exercise 4.2
	Solution to exercise 4.3
List of Notations
Index of Programs
References
Index
Other titles from iSTE in Computer Engineering
EULA