Abstract
This short note compares two different methods for exploring type-inhabitation in the simply typed lambda-calculus, highlighting their similarities.

Abstract
We define a framework for the analysis of access control policies that aims at easing the specification and verification tasks for security administrators. We consider policies in the category-based access control model, which has been shown to subsume many of the most well known access control models (e.g., MAC, DAC, RBAC). Using a graphical representation of category-based policies, we show how answers to usual administrator queries can be automatically computed, and properties of access control policies can be checked. We show applications in the context of emergency situations, where our framework can be used to analyse the interaction between access control and emergency management.

Abstract
We present a new type system combining refinement types and the expressiveness of intersection type discipline. The use of such features makes it possible to derive more precise types than in the original refinement system. We have been able to prove several interesting properties for our system (including subject reduction) and developed an inference algorithm, which we proved to be sound.

Abstract
We define a general typed language to deal with the notion of event in the context of access control systems. We distinguish between generic events, which represent the kind of actions that can occur in a system, and specific events, which represent actual occurrences of those kinds of actions. A relation is given associating specific to generic events, as well as a method for obtaining intervals from a history of events. We describe applications in access control systems with obligations.

Abstract
The use of unmanned vehicle networks for diverse applications is becoming widespread. It is generally hard to program unmanned vehicle networks as a "whole", however. The coordination of multiple vehicles requires careful planning through intricate human intervention, and a high degree of informality is implied in what concerns the specification of a "network program" for an application scenario. In this context, we have been developing a programming language for expressing global specifications of coordinated behavior in unmanned vehicle networks, the Networked Vehicles' Language (NVL). In this paper we illustrate the use of the language for a thermal pollution plume tracking scenario employing unmanned underwater vehicles.

Abstract
The coordinated use of multiple unmanned vehicles over a network can be employed for numerous real-world applications. However, multi-vehicle operations are often deployed through a patchwork of separate components that informally "glue" together during operation, as they are hard to program as a "whole". With this aim, we developed the Networked Vehicles' Language (NVL) for coordinated control of unmanned vehicle networks. A single NVL program expresses an on-the-fly selection of multiple vehicles and their allocation to cooperative tasks, subject to time, precedence, and concurrency constraints. We present the language through an example application involving unmanned underwater vehicles (UUVs) and unmanned aerial vehicles (UAVs), the core design and implementation traits, and results from simulation and field test experiments.