Abstract
The present Special Issue of the Journal of Logical and Algebraic Methods in Programming was planned as a tribute to Jose Manuel Esgalhado Valenca on the occasion of his Jubilation. A tribute to a professor, in the deepest sense of the word, a colleague and a friend, but above all to a long and inspiring academic journey that has so profoundly shaped the development of Informatics as a scientific area in Portugal. A scientific area that, as he taught us, needs to be understood broadly: not only as an independent research domain, but also as an educational pillar, a strategy for social and economic development, a foundation for a multifaceted professional career. This preface introduces some steps of such a journey. The Special Issue features a selection of scientific papers written by his collaborators, colleagues and friends, covering the different areas Jose Valenca helped to launch and consolidate in Portugal, namely computational logic, verification and mechanized reasoning, and information security. (c) 2022 Published by Elsevier Inc.

Abstract
Alloy is a popular language and tool for formal software design. A key factor to this popularity is its relational logic, an elegant specification language with a minimal syntax and semantics. However, many software problems nowadays involve both structural and quantitative requirements, and Alloy's relational logic is not well suited to reason about the latter. This paper introduces QAlloy, an extension of Alloy with quantitative relations that add integer quantities to associations between domain elements. Having integers internalised in relations, instead of being explicit domain elements like in standard Alloy, allows quantitative requirements to be specified in QAlloy with a similar elegance to structural requirements, with the side-effect of providing basic dimensional analysis support via the type system. The QAlloy Analyzer also implements an SMT-based engine that enables quantities to be unbounded, thus avoiding many problems that may arise with the current bounded integer semantics of Alloy.

Abstract
Models-at different levels of abstraction and pertaining to different engineering views-are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone. This paper presents EVEREST, a tool for automating the verification of railway network models that preserves the loosely coupled nature of the design process. To achieve this goal, EVEREST first combines two different views of a railway network model-the topology provided in signalling diagrams containing the functional infrastructure, and the precise coordinates of the elements provided in technical drawings (CAD)-in a unified model stored in the railML standard format. This railML model is then verified against a set of user-defined infrastructure rules, written in a custom modal logic that simplifies the specification of spatial constraints in the network. The violated rules can be visualized both in the signalling diagrams and technical drawings, where the element(s) responsible for the violation are highlighted. EVEREST is integrated in a long-term effort of EFACEC to implement industry-strong tools to automate and formally verify the design of railway solutions. © 2022 ACM.

Abstract
Based on the connection between the categorical derivation of classical programs from specifications and a category-theoretic approach to quantum information, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at building correct-by-construction quantum circuits to be deployed on quantum devices such as those available through the IBM Q Experience. Reversibility is ensured by minimal complements. Such complementation is extended inductively to encompass catamorphisms on lists (vulgo folds), giving rise to the corresponding recursion scheme in reversible computation. The same idea is then applied to the setting of quantum programming, where computation is expressed by unitary transformations. This yields the notion of 'quantamorphism', a structural form of quantum recursion implementing cycles and folds on lists with quantum control flow. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. Such calculated quantum programs prepared in Haskell are pushed through Quipper and the Qiskit interface to IBM Q quantum devices. The generated quantum circuits - often quite large - exhibit the predicted behaviour. However, running them on real quantum devices naturally incurs a significant amount of errors. As quantum technology is rapidly evolving, an increase in reliability is likely in the future, allowing for our programs to run more accurately.

Abstract
We study a simple inductive data type for representing correct-by-construction matrices. Despite its simplicity, it can be used to implement matrix-manipulation algorithms efficiently and safely, performing in some cases faster than existing alternatives even though the algorithms are written in a direct and purely functional style. A rich collection of laws makes it possible to derive and optimise these algorithms using equational reasoning, avoiding the notorious off-by-one indexing errors when fiddling with matrix dimensions. We demonstrate the usefulness of the data type on several examples, and highlight connections to related topics in category theory. © 2020 ACM.