Control Structures for Programming Languages

Autorentext

Xavier Leroy is Professor of Software Sciences at Collège de France. He is known for his work on OCaml, a popular functional programming language, and CompCert, the first formally verified C compiler. He is a member of the French Academy of Sciences and a Fellow of the ACM.

Klappentext

An exploration of the design space and development of programming languages from the perspective of control structures: the language mechanisms that enable programs to control their execution flows. Starting with the 'goto' jumps of early programming languages and the emergence of structured programming in the 1960s, this book explores advanced control structures for imperative languages such as generators and coroutines, then develops alternate views of control in functional languages, first as continuations and their control operators, then as algebraic effects and effect handlers, as found in the OCaml language. Blending history, code examples, and theory, it offers advanced students, researchers, and programming language enthusiasts an original, comparative perspective on programming languages, as well as an extensive introduction to algebraic effects and other contemporary research topics.

Inhalt

Preface; Introduction; Part I. Control Structures for Imperative Languages: 1. Early programming languages; 2. Structured programming; 3. Non-local control: Subroutines, procedures, functions; 4. Control inversion: Iterators, generators, coroutines; Part II. Control Operators for Functional Languages: 5. Functional languages; 6. Continuations and the CPS transformation; 7. Programming with continuations; 8. Control operators; Part III. From Exceptions to Algebraic Effects and Handlers: 9. Exceptions; 10. Effect handlers for user-de ned effects; 11. Monads; 12. Algebraic effects; Part IV. Reasoning about Control and Effects: 13. Type and effect systems; 14. Hoare logic for control structures; 15. Separation logic for control operators; Bibliography; Index.