Le raccolte fotografiche per la didattica artistica: fonti e strumenti archivistici per la ricerca

Displayed universal algebra in UniMath: basic definitions and results

Univalent mathematics and homotopy type theory provide a structural approach to formalizing mathematical concepts. Inspired by the role of displayed categories in the univalent treatment of category theory, we develop an analogous notion of displayed algebras for universal algebra. This modular and layered approach allows us to construct and reason about algebraic structures over a fixed base. Classical constructions such as cartesian products, pullbacks, semidirect products, and subalgebras ...

A modular proof of semantic completeness for normal systems beyond the modal cube, formalised in HOLMS

We communicate here the most recent extension of HOLMS, our library for modal logics aimed at introducing automated modal reasoning within the HOL Light proof assistant. Based on a uniform proof strategy, we present a more refined formal proof of completeness for systems within and beyond the S5-normal modal cube, notably Gödel-Löb logic. We report on our development by adopting a measure of its modularity based on Strachey's distinction between parametric and ad hoc polymorphic code.

A model-based approach for cybersecurity assessment of off-road and defense vehicles

The large amount of Electric/Electronic (E/E) systems in modern vehicles make them vulnerable to cyberattacks. New regulations and standards, such as UNECE R155 and ISO/SAE 21434, aim to tackle this issue by providing tools and workflows that vehicle designers can use to minimize cybersecurity threats. Plenty of research is being carried out in the automotive cybersecurity field, which is rich in assessment methodologies that comply with latest regulations. However, most efforts focus on Conn...