Abstract

Abstract
Weak linearisation was defined years ago through a static characterization of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between “consumed” and “persistent” term constructors, which allows us to define an expansion relation, between general ? -terms and weak-linear ? -terms, whilst preserving normal forms by reduction. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative, commutative and idempotent intersections with terms typed in the Curry type system and the relevant type system; terms typed by non-idempotent intersections with terms typed in the affine and linear type systems; and terms typed by non-idempotent and non-commutative intersections with terms typed in an ordered type system. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
Non-idempotent intersection types provide quantitative information about typed programs, and have been used to obtain time and space complexity measures. Intersection type systems characterize termination, so restrictions need to be made in order to make typability decidable. One such restriction consists in using a notion of finite rank for the idempotent intersection types. In this work, we define a new notion of rank for the non-idempotent intersection types. We then define a novel type system and a type inference algorithm for the ?-calculus, using the new notion of rank 2. In the second part of this work, we extend the type system and the type inference algorithm to use the quantitative properties of the non-idempotent intersection types to infer quantitative information related to resource usage. © Fábio Reis, Sandra Alves, and Mário Florido.

Abstract

Abstract
The Internet of Things (IoT) has changed how we interact with the world around us. Many devices are moving from offline to online mode, connecting between them and the Internet, offering more functionality to users. Despite the increase in the quality of life for users provided by IoT devices, it is also necessary to establish trust in the privacy and security of end-users. With this level of connectivity, the amount of data exchanged between devices also increases, inducing malicious activities. One of the main problems is the lack of regulation in the IoT industry, especially between different manufacturers. There are no formal security rules, and manufacturers may not choose to install security mechanisms. Therefore, it is necessary to promote the adoption of security measures. One way to do this is by using IoT devices and systems certification. In recent years, IoT certifications have emerged. Meanwhile, the European Union has passed the Cyber Security Act to unify and regulate security certifications in member states. Our work collects the requirements that different IoT environments and application scenarios impose on certifications and discusses the current certifications' status according to those requirements. In addition, we also explored how EU measures apply to IoT and, where applicable, how certifications implement them, highlighting future research challenges.