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
The deep-sea covers over 70% of the Earth’s surface and harbors predominantly uncharacterized bacterial communities. Actinobacteria are the major prokaryotic source of bioactive natural products that find their way into drug discovery programs, and the deep-sea is a promising source of biotechnologically relevant actinobacteria. Previous studies on actinobacteria in deep-sea sediments were either regionally restricted or did not combine a community characterization with the analysis of their bioactive potential. Here we characterized the actinobacterial communities of upper layers of deep-sea sediments from the Arctic and the Atlantic (Azores and Madeira) ocean basins, employing 16S rRNA metabarcoding, and studied the biosynthetic potential of cultivable actinobacteria retrieved from those samples. Metabarcoding analysis showed that the actinobacterial composition varied between the sampled regions, with higher abundance in the Arctic samples but higher diversity in the Atlantic ones. Twenty actinobacterial genera were detected using metabarcoding, as a culture-independent method, while culture-dependent methods only allowed the identification of nine genera. Isolation of actinobacteria resulted on the retrieval of 44 isolates, mainly associated with Brachybacterium, Microbacterium, and Brevibacterium genera. Some of these isolates were only identified on a specific sampled region. Chemical extracts of the actinobacterial isolates were subsequently screened for their antimicrobial, anticancer and anti-inflammatory activities. Extracts from two Streptomyces strains demonstrated activity against Candida albicans. Additionally, eight extracts (obtained from Brachybacterium, Brevibacterium, Microbacterium, Rhodococcus, and Streptomyces isolates) showed significant activity against at least one of the tested cancer cell lines (HepG2 and T-47D). Furthermore, 15 actinobacterial extracts showed anti-inflammatory potential in the RAW 264.4 cell model assay, with no concomitant cytotoxic response. Dereplication and molecular networking analysis of the bioactive actinobacterial extracts showed the presence of some metabolites associated with known natural products, but one of the analyzed clusters did not show any match with the natural products described as responsible for these bioactivities. Overall, we were able to recover taxonomically diverse actinobacteria with different bioactivities from the studied deep-sea samples. The conjugation of culture-dependent and -independent methods allows a better understanding of the actinobacterial diversity of deep-sea environments, which is important for the optimization of approaches to obtain novel chemically-rich isolates. Copyright © 2023 Ribeiro, Antunes, Alexandrino, Tomasino, Almeida, Hilário, Urbatzka, Leão, Mucha and Carvalho.

Abstract
Innovation plays a key role in meeting the challenges of the future, but despite the unprecedented investment in innovation, Portugal has seen a decline in the various indicators that assess the country's performance. This study aims to answer questions about the state of innovation in Portugal, based on the relevant global and European innovation indicators, comparing the country's performance with that of Ireland, Belgium, and the Czech Republic. Using secondary data collected from the reports of the last four years, explanatory research was conducted based on statistical and graphical methods in order to establish causal relationships. The areas where the main changes have taken place are presented, highlighting the aspects in which Portugal stands out for superior or poor performance, providing a benchmark for the definition of policies to foster innovation in Portugal. The results demonstrate that institutions, business sophistication, and knowledge and technology score negatively, while creativity stands out as a strength. Environmental sustainability, firms' investment in innovation, and the impact of innovation on sales are aspects that Portugal needs to improve; human capital and the attractiveness of the R & D system deserve positive remarks. It is fundamental to understand how Portugal is preparing for the future and what the country can learn from others. This study is limited by the specific period in analysis, which could affect causal relationships, and the historical perspective could provide guidelines to the understanding of the relative position of the country. This study contributes new perspectives and knowledge about the state of innovation in Portugal, providing clues to entrepreneurs, policy makers, and the scientific community.

Abstract

Abstract
In the evolving landscape of global education, Artificial Intelligence's (AI) integration into Learning Management Systems (LMS) promises a transformative shift. This paper presents Mozambique's journey in this domain, comparing it with global advancements. While the Mozambican higher education sector stands at the cusp of a digital revolution, its engagement with AI in LMS remains foundational. This is juxtaposed against the global trend where AI tools, such as ChatGPT, are rapidly becoming standard in many educational platforms, enhancing personalization, efficiency, and data-driven insights. The benefits of AI integration, such as tailored learning experiences and administrative automation, are counterbalanced by challenges, including data privacy concerns and over-reliance on technology. Drawing from real-world case studies, the paper highlights pioneering endeavours that showcase AI's potential in reshaping educational paradigms. As Mozambique navigates its unique challenges, insights from global best practices offer a roadmap for harnessing the transformative potential of AI in LMS, aiming to elevate its higher education sector to new heights.;Na evolução da educação global, a integração da Inteligência Artificial (IA) nos Sistemas de Gestão de Aprendizagem (LMS) promete uma transformação significativa. Este artigo investiga a jornada de Moçambique neste domínio, comparando-a com os avanços globais. Enquanto o setor de ensino superior moçambicano está à beira de uma revolução digital, seu envolvimento com a IA em LMS ainda está em uma fase inicial. Isso é contrastado com a tendência global, onde ferramentas de IA, como o ChatGPT, estão rapidamente se a se tornar padrão em muitas plataformas educativas, aprimorando a personalização, eficiência e insights baseados em dados. Os benefícios da integração da IA, como experiências de aprendizagem adaptadas e automação administrativa, são equilibrados por desafios, incluindo preocupações com a privacidade dos dados e excesso de dependência da tecnologia. Através de estudos de caso do mundo real, o artigo destaca esforços pioneiros que mostram o potencial da IA em remodelar os paradigmas educacionais. Enquanto Moçambique navega pelos seus desafios únicos, os insights das melhores práticas globais oferecem um roteiro para aproveitar o potencial transformador da IA em SGA, com o objetivo de elevar seu setor de ensino superior a novos patamares.

Abstract
Global warming presents a significant threat to the sustainability of agricultural systems, demanding increased irrigation to mitigate the impacts of prolonged dry seasons. Efficient water management strategies, including deficit irrigation, have thus become essential, requiring continuous crop monitoring. However, conventional monitoring methods are laborious and time-consuming. This study investigates the potential of aerial imagery captured by unmanned aerial vehicles (UAVs) to predict critical water stress indicators-relative water content (RWC), midday leaf water potential (psi MD), stomatal conductance (gs)-as well as the pigment content (chlorophyll ab, chlorophyll a, chlorophyll b and carotenoids) of trees in an olive orchard. Both thermal and spectral vegetation indices are calculated and correlated using linear and exponential regression models. The results reveal that the thermal vegetation indices contrast in estimating the water stress indicators, with the Crop Water Stress Index (CWSI) demonstrating higher precision in predicting the RWC (R2 = 0.80), psi MD (R2 = 0.61) and gs (R2 = 0.72). Additionally, the Triangular Vegetation Index (TVI) shows superior accuracy in predicting the chlorophyll ab (R2 = 0.64) and chlorophyll a (R2 = 0.61), while the Modified Chlorophyll Absorption in Reflectance Index (MCARI) proves most effective for estimating the chlorophyll b (R2 = 0.52). This study emphasizes the potential of UAV-based multispectral and thermal infrared imagery in precision agriculture, enabling assessments of the water status and pigment content. Moreover, these results highlight the vital importance of this technology in optimising resource allocation and enhancing olive production, critical steps towards sustainable agriculture in the face of global warming.