Abstract
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.

Abstract
Archives preserve materials that allow us to understand and interpret the past and think about the future. With the evolution of the information society, archives must take advantage of technological innovations and adapt to changes in the kind and volume of the information created. Semantic Web representations are appropriate for structuring archival data and linking them to external sources, allowing versatile access by multiple applications. ArchOnto is a new Linked Data Model based on CIDOC CRM to describe archival objects. ArchOnto combines specific aspects of archiving with the CIDOC CRM standard. In this work, we analyze the ArchOnto representation of a set of archival records from the Portuguese National Archives and compare it to their CIDOC CRM representation. As a result of ArchOnto's representation, we observe an increase in the number of classes used, from 20 in CIDOC CRM to 28 in ArchOnto, and in the number of properties, from 25 in CIDOC CRM to 28 in ArchOnto. This growth stems from the refinement of object types and their relationships, favouring the use of controlled vocabularies. ArchOnto provides higher readability for the information in archival records, keeping it in line with current standards.

Abstract

Abstract
This work addresses a variant of the job shop scheduling problem in which jobs need to be transported to the machines processing their operations by a limited number of vehicles. Given that vehicles must deliver the jobs to the machines for processing and that machines need to finish processing the jobs before they can be transported, machine scheduling and vehicle scheduling are intertwined. A coordi-nated approach that solves these interrelated problems simultaneously improves the overall performance of the manufacturing system. In the current competitive business environment, and integrated approach is imperative as it boosts cost savings and on-time deliveries. Hence, the job shop scheduling problem with transport resources (JSPT) requires scheduling production operations and transport tasks simultane-ously. The JSPT is studied considering the minimization of two alternative performance metrics, namely: makespan and exit time. Optimal solutions are found by a mixed integer linear programming (MILP) model. However, since integrated production and transportation scheduling is very complex, the MILP model can only handle small-sized problem instances. To find good quality solutions in reasonable com-putation times, we propose a hybrid particle swarm optimization and simulated annealing algorithm (PSOSA). Furthermore, we derive a fast lower bounding procedure that can be used to evaluate the perfor-mance of the heuristic solutions for larger instances. Extensive computational experiments are conducted on 73 benchmark instances, for each of the two performance metrics, to assess the efficacy and efficiency of the proposed PSOSA algorithm. These experiments show that the PSOSA outperforms state-of-the-art solution approaches and is very robust.(c) 2022 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY-NC-ND license ( http://creativecommons.org/licenses/by-nc-nd/4.0/ )

Abstract
E-commerce growth is raising the demand for logistic activities, especially in the last-mile, which is considered the most ineffective part of the supply chain and a negative externalities source. Although various solutions aim to address these issues, selecting the best one is challenging due to multiple perspectives, conflicting criteria, trade-offs, and complex and sensitive urban contexts. This article proposes a 4-level hierarchical model based on the triple bottom line of sustainability that may assist decision-makers in selecting the most adequate last -mile solution for historic centers. The model was defined based on a systematic literature review; evaluated by interviewing a set of experts; and quantified according to an AHP-TOPSIS approach. This quantification focused on the historic center of Porto, Portugal. The experts considered all three sustainability dimensions similarly important. Air pollution was the most valued sub-criterion whereas Visual pollution was the least. 67 decision-maker profiles were defined, showing that environmentally oriented decision-makers prefer cargo bikes, while decision-makers who prioritize economic and social factors prefer parcel lockers. All last-mile solutions considered in the model yielded similar results, therefore suggesting a combined distribution strategy. Nevertheless, the use of parcel lockers is the most favorable solution for Porto's historic center.

Abstract
In this letter, a new configuration based on two fiber loop mirrors in series using a 3x3 coupler is demonstrated. This configuration is compact and can explore the Vernier effect. The results obtained were a sensitivity of 74.9 +/- 0.2 pm/ mu epsilon for the Vernier envelope and 6.41 +/- 0.01 pm/mu epsilon for the Vernier carrier. These results were compared to the sensitivity of the setup using only one fiber loop mirror interferometer, obtaining 14.41 +/- 0.01 pm/mu epsilon. This means a magnification factor of 5.2 for the Vernier envelope. Theoretical treatment of the system was carried out, using Jones matrix calculus, and the subsequent simulation results are also presented, having obtained good agreement with the experimental data.