In this paper, we report some of the activities carried on in the last years by the research group leaded by Alberto Martelli. In particular, it presents a research line that encompasses the specification, the development and the verification of interaction protocols. The leading thread is given by the use of multimodal logics and of declarative formalisms and reasoning techniques, based on computational logic.