This festschrift celebrates Nissim Francez's 65th birthday. It covers a wide variety of articles on linguistics and the foundations of verification, written by top people in the field. This review only discusses the contributions the reviewer found most interesting.

Apt, de Boer and Olderog's “Modular verification of recursive programs” looks afresh at classical Hoare-style verification, studying how an existing proof of a program can be used to develop a more incisive proof of the same program. The authors depart from traditional compositional reasoning to a style which is more reminiscent of the use of modus ponens.

In “Nonassociative Lambek calculus with additives and context-free languages,” Buszkowski and Farulewski show that categorial grammars based on distributive full nonassociative Lambek calculus generate context-free languages (CFLs). On the other hand, full nonassociative Lambek calculus goes beyond CFLs.

Elrad's paper, “Aspect oriented approach for capturing and verifying distributed properties,” compares distributed programs made up of communication-closed layers (developed with Francez in 1982)—and aspects.

In “Classes of service under perfect competition and technological change,” Daniel Lehmann attempts an ambitious exercise to analyze and predict the evolution of the internet.

Pratt-Hartmann's paper, “No syllogisms for the numerical syllogistic,” shows that a numerical syllogistic has no finite axiomatization.

On the linguistic side, I enjoyed reading Wintner et al's “Formal grammars of early language” for its experimental approach to the development of grammar in child language development.

In summary, libraries should look to acquire this book for their collections.