Concepts and Semantics of Programming Languages 1
A Semantical Approach with OCaml and Python
1st Edition
Published on 13. April 2021
336 pages
978-1-119-82404-6 (ISBN)
Description
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.
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.
More details
Other editions
Additional editions
HARDIN | Mathieu Jaume | Pessaux
Concepts and Semantics of Programming Languages 1: A Semantical Approach with Ocaml and Python
A Semantical Approach with OCaml and Python
Book
08/2021
ISTE Ltd
€164.50
Shipment within 3-4 weeks
Persons
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.
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.
Content
- 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
