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

ISBN-13: 9781786305305 / Angielski / Twarda / 2021 / 336 str.

Hardin; Mathieu Jaume;Pessaux

Spis treści

Foreword xiPreface xiiiChapter 1. From Hardware to Software 11.1. Computers: a low-level view 11.1.1. Information processing 11.1.2. Memories 21.1.3. CPUs 31.1.4. Peripheral devices 71.2. Computers: a high-level view 81.2.1. Modeling computations 91.2.2. High-level languages 91.2.3. From source code to executable programs 10Chapter 2. Introduction to Semantics of Programming Languages 152.1. Environment, memory and state 162.1.1. Evaluation environment 162.1.2. Memory 182.1.3. State 202.2. Evaluation of expressions 212.2.1. Syntax 212.2.2. Values 222.2.3. Evaluation semantics 242.3. Definition and assignment 262.3.1. Defining an identifier 262.3.2. Assignment 292.4. Exercises 31Chapter 3. Semantics of Functional Features 353.1. Syntactic aspects 353.1.1. Syntax of a functional kernel 353.1.2. Abstract syntax tree 363.1.3. Reasoning by induction over expressions 393.1.4. Declaration of variables, bound and free variables 393.2. Execution semantics: evaluation functions 423.2.1. Evaluation errors 423.2.2. Values 433.2.3. Interpretation of operators 453.2.4. Closures 463.2.5. Evaluation of expressions 473.3. Execution semantics: operational semantics 543.3.1. Simple expressions 553.3.2. Call-by-value 563.3.3. Recursive and mutually recursive functions 603.3.4. Call-by-name 613.3.5. Call-by-value versus call-by-name 623.4. Evaluation functions versus evaluation relations 643.4.1. Status of the evaluation function 643.4.2. Induction over evaluation trees 653.5. Semantic properties 693.5.1. Equivalent expressions 693.5.2. Equivalent environments 713.6. Exercises 71Chapter 4. Semantics of Imperative Features 774.1. Syntax of a kernel of an imperative language 774.2. Evaluation of expressions 814.3. Evaluation of definitions 864.4. Operational semantics 894.4.1. Big-step semantics 894.4.2. Small-step semantics 934.4.3. Expressiveness of operational semantics 954.5. Semantic properties 964.5.1. Equivalent programs 964.5.2. Program termination 984.5.3. Determinism of program execution 1004.5.4. Big steps versus small steps 1034.6. Procedures 1094.6.1. Blocks 1094.6.2. Procedures 1124.7. Other approaches 1184.7.1. Denotational semantics 1184.7.2. Axiomatic semantics, Hoare logic 1294.8. Exercises 134Chapter 5. Types 1375.1. Type checking: when and how? 1395.1.1. When to verify types? 1395.1.2. How to verify types? 1405.2. Informal typing of a program Exp2 1415.2.1. A first example 1415.2.2. Typing a conditional expression 1425.2.3. Typing without type constraints 1425.2.4. Polymorphism 1435.3. Typing rules in Exp2 1435.3.1. Types, type schemes and typing environments 1435.3.2. Generalization, substitution and instantiation 1465.3.3. Typing rules and typing trees 1515.4. Type inference algorithm in Exp2 1545.4.1. Principal type 1545.4.2. Sets of constraints and unification 1555.4.3. Type inference algorithm 1595.5. Properties 1675.5.1. Properties of typechecking 1675.5.2. Properties of the inference algorithm 1675.6. Typechecking of imperative constructs 1685.6.1. Type algebra 1685.6.2. Typing rules 1695.6.3. Typing polymorphic definitions 1715.7. Subtyping and overloading 1725.7.1. Subtyping 1735.7.2. Overloading 175Chapter 6. Data Types 1796.1. Basic types 1796.1.1. Booleans 1796.1.2. Integers 1816.1.3. Characters 1866.1.4. Floating point numbers 1876.2. Arrays 1916.3. Strings 1946.4. Type definitions 1946.4.1. Type abbreviations 1956.4.2. Records 1966.4.3. Enumerated types 2006.4.4. Sum types 2026.5. Generalized conditional 2056.5.1. C style switch/case 2056.5.2. Pattern matching 2086.6. Equality 2166.6.1. Physical equality 2176.6.2. Structural equality 2186.6.3. Equality between functions 220Chapter 7. Pointers and Memory Management 2237.1. Addresses and pointers 2237.2. Endianness 2257.3. Pointers and arrays 2257.4. Passing parameters by address 2267.5. References 2297.5.1. References in C++ 2297.5.2. References in Java 2337.6. Memory management 2347.6.1. Memory allocation 2347.6.2. Freeing memory 2377.6.3. Automatic memory management 239Chapter 8. Exceptions 2438.1. Errors: notification and propagation 2438.1.1. Global variable 2458.1.2. Record definition 2458.1.3. Passing by address 2458.1.4. Introducing exceptions 2468.2. A simple formalization: ML-style exceptions 2478.2.1. Abstract syntax 2478.2.2. Values 2488.2.3. Type algebra 2488.2.4. Operational semantics 2488.2.5. Typing 2508.3. Exceptions in other languages 2508.3.1. Exceptions in OCaml 2518.3.2. Exceptions in Python 2518.3.3. Exceptions in Java 2538.3.4. Exceptions in C++ 254Conclusion 257Appendix: Solutions to the Exercises 259List of Notations 287Index of Programs 289References 293Index 295

O autorze

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.