Bøker i Foundations and Trends (R) in Programming Languages-serien

Examines the progress properties of concurrent objects. The book formulates each progress property in terms of contextual refinement so that, when verifying clients of the objects, concrete object implementations can be replaced with their abstractions with certainty, achieving modular verification.

Covers the timeline and research literature concerning proof development for program verification, including theories, languages, and tools. The book emphasizes challenges and breakthroughs at each stage in history and highlights challenges that are currently present due to the increasing scale of proof developments.

Provides a comprehensive introduction to the field of shape analysis, and presents the foundation of the topic in an accessible manner to readers who are not familiar with it. To do so, the authors characterize the essence of shape analysis compared to more classical pointer analyses.

Inspired by the nanopass framework for teaching compilation, this book shows how to implement refinement types via a progression of languages that incrementally add features to the language or type system. The book provides an insightful introduction into Refinement Types using an innovative tutorial style that enables fast learning.

The comprehensive review of neurosymbolic programming introduces the reader to the topic and provides an insightful treatise on an increasingly important topic at the intersection of programming languages and machine learning.