Abstract

Abstract
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale V, which covers the cases of (in)equations and (ultra)metric equations among others.Our main result is the introduction of a V-equational deductive system for linear lambda-calculus together with a proof that it is sound and complete. In fact we go further than this, by showing that linear lambda-theories based on this V-equational system form a category equivalent to a category of autonomous categories enriched over 'generalised metric spaces'. If we instantiate this result to inequations, we get an equivalence with autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an equivalence with autonomous categories enriched over (ultra)metric spaces. Additionally, we show that this syntax-semantics correspondence extends to the affine setting.We use our results to develop examples of inequational and metric equational systems for higher-order programming in the setting of real-time, probabilistic, and quantum computing.

Abstract

Abstract
The digitalization of energy generation and distribution systems opens new opportunities for devising network operation and traffic engineering strategies capable of adapting to the energy availability and sources. Despite the potential, developing and testing new approaches are challenging in production environments. Furthermore, no simulators support such integration between the communication infrastructure and the power grid. Thus, this paper introduces Flexcomm Simulator, a tool based on ns-3 that supports developing and assessing multiple strategies toward green networking and communications driven by real-time information from the power grid (i.e., Energy Flexibility). The proof-of-concept results demonstrate this contribution's potential by implementing an energy-aware routing algorithm that adapts to real-world Energy Flexibility data in a Metropolitan Area Network (MAN). Also, it showcases the simulator's capacity to deal with large-scale simulations through MPI-based distributed environments.

Abstract
This paper presents GLITCH, a new technology-agnostic framework that enables automated polyglot code smell detection for Infrastructure as Code scripts. GLITCH uses an intermediate representation on which different code smell detectors can be defined. It currently supports the detection of nine security smells and nine design & implementation smells in scripts written in Ansible, Chef, Docker, Puppet, or Terraform. Studies conducted with GLITCH not only show that GLITCH can reduce the effort of writing code smell analyses for multiple IaC technologies, but also that it has higher precision and recall than current state-of-the-art tools. A video describing and demonstrating GLITCH is available at: https://youtu.be/E4RhCcZjWbk.

Abstract
We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference - the latter being a variant of Nelson's biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non -monotonic program combinators.