Andrew W. Appel Knihy

Focusing on separation logic, this book provides a comprehensive introduction to both practical and theoretical aspects of software verification, particularly for pointer-manipulating programs. It includes case studies in Hoare and separation logics, along with practical applications in the Verifiable C program logic. Theoretical discussions cover separation algebras, step-indexed models, and tree-shares. Additionally, it explores the CompCert verified C compiler and its relation to verified software analysis tools, all rigorously supported by Coq developments in the Verified Software Toolchain.

Continuations serve as a powerful tool for representing control and data flow in programming, with significant applications in compiler design. This book explores the use of continuation-passing style as an intermediate representation for optimizing and transforming programs, specifically demonstrated through a compiler for Standard ML. It is accessible to readers without prior ML knowledge, as each concept is thoroughly explained. Aimed at compiler writers, students, and researchers, it bridges theoretical programming language concepts with practical compiler development.

Focusing on the intricacies of modern compilers, this book covers all phases of compilation, emphasizing techniques for code generation and register allocation. It addresses various programming paradigms, including imperative, functional, and object-oriented languages, providing a comprehensive understanding of how compilers work across different contexts.

The book provides a comprehensive overview of modern compiler design, detailing each phase of compilation. It covers essential techniques such as code generation and register allocation, applicable to various programming paradigms, including imperative, functional, and object-oriented languages. This resource serves as a valuable guide for understanding the complexities of compiler construction and optimization.