Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems - Yamine Ait-Ameur, Shin Nakajima, Dominique Méry (Springer, 2021)