Bücher der Reihe Foundations and Trends (R) in Programming Languages

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.

It is well documented that fully automatic rigorous verification of complex software is very challenging and perfection is impossible. This book presents abstract interpretation and shows how its principles can be successfully applied to cope with the difficulties inherent to formal verification.

The successful application of behavioural types requires an understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs, to design and monitoring methodologies. This book provides the reader with a comprehensive overview of these practical aspects.

Provides the reader with a tutorial on some modern techniques to model and automatically analyse security protocols. Given the large body of work in this area, it does not aim to be exhaustive so the focus is on some selected methods and results.

Examines both the what and the how of consistency in distributed systems. The book provides the reader with tools for reasoning about consistency of protocols. The emphasis is on using basic mathematical techniques to describe a wide variety of consistency guarantees and to define protocols.

Modular heap analysis techniques analyse a program by computing summaries for every procedure in the program that describes its effects on an input heap. This book focuses on modular heap analyses that summarize a procedure's heap effects using a context-independent, shape-graph-like summary that is agnostic to the aliasing in the input heap.

Complements existing introductory literature to game semantics, which highlight the then new structural components necessary to model higher-order computation; for example, arenas, justification pointers, and innocence. In contrast, this monograph focuses on explaining the nominal content of our games.

Describes a set of technologies that assist users in specifying database queries for different application domains. The goal of such systems is to bridge the gap between current query interfaces provided by database management systems and the needs of different usage scenarios that are not well served by existing query languages.

The vast amount of code available on the web is increasing daily. Open-source hosting sites contain billions of lines of code. Community question-answering sites provide millions of code snippets with corresponding text and metadata. The amount of code available in executable binaries is even greater.

Assuming no prior knowledge of MetaOCaml and only a basic familiarity with functional programming, this book explains and illustrates how to implement a simple domain-specific language for linear algebra, with layers of optimizations for sparsity and memory layout of matrices and vectors, and their algebraic properties.

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 book is a self-contained treatment of a topic that sits at the intersection of machine learning and formal verification. It can serve as an introduction to the field for first-year graduate students or senior undergraduates, even if they have not been exposed to deep learning or verification.

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.