Search

Dynamic typed languages are characterized by their expressiveness and flexibility to develop prototypes, while static typed languages allow early detection of errors and the optimization of source code. Gradual typing languages allow programmers to make use of both approaches, static and dynamic typing, and thus, obtaining the advantages that both represent. The objective here is to revisit the static part of the approach to a gradual interpretation of union types based on the design of Gradual Union Types through an extension with the record data-structure. This contributes to understand the abstraction and reasoning behind Gradual Typing in order to have useful future extensions for other data-structures.

Logic Programming and fuzzy logic are active areas of research, and their scopes in terms of applications are growing fast. Fuzzy logic is a branch of many-valued logic based on the paradigm of inference under vagueness. In this work we recall some of the interplay between three 3-valued logics that are relevant in these areas: The Lukasiewicz logic, the intermediate logic G3 and the paraconsistent logic G 3 ′ , and we present a contribution to the area of answer sets that consists in extending a definition of stable model based on proof theory in logic G3, to a more general definition that can be based on any of the more expressive logics G 3 ′ or Lukasiewicz. Finally we present and explore a new 4-valued logic that bears relation to G3 and to Lukasiewicz 4-valued logic.

Answer Set Programming (ASP) is a successful rule-based formalism for modeling and solving knowledge-intense combinatorial (optimization) problems. Despite its success in both academic and industry, open challenges like automatic source code optimization, and software engineering remains. This is because a problem encoded into an ASP might not have the desired solving performance compared to an equivalent representation. Motivated by these two challenges, this paper has three main contributions. First, we propose a developing process towards a methodology to implement ASP programs, being faithful to existing methods. Second, we present ASP encodings that serve as the basis from the developing process. Third, we demonstrate the use of ASP to reverse the standard solving process. That is, knowing answer sets in advance, and desired strong equivalent properties, “we” exhaustively reconstruct ASP programs if they exist. This paper was originally motivated by the search of propositional formulas (if they exist) that represent the semantics of a new aggregate operator. Particularly, a parity aggregate. This aggregate comes as an improvement from the already existing parity ( xor ) constraints from xorro, where lacks expressiveness, even though these constraints fit perfectly for reasoning modes like sampling or model counting. To this end, this extended version covers the fundaments from parity constraints as well as the xorro system. Hence, we delve a little more in the examples and the proposed methodology over parity constraints. Finally, we discuss our results by showing the only representation available, that satisfies different properties from the classical logic xor operator, which is also consistent with the semantics of parity constraints from xorro.

We evaluate energy consumption under unknown service demands using three policies: task assignment based on guessing size (TAGS), the shortest queue strategy and random allocation in a homogeneous environment. We modelled these policies using performance evaluation processing algebra (PEPA) to derive numerical solutions. Our results show that servers running under TAGS consumes more energy than other policies in terms of total energy consumption. In contrast, TAGS consumes less energy than random allocation in terms of energy per job when the arrival rate is high and the job size is variable.

In this paper we present two performance models of a web-based sales system, one without the presence of an attack and the other with the presence of a denial of service attack. Models are formulated using the PEPA formalism. The PEPA eclipse plug-in is used to support the creation of the PEPA models for the web-based sales system and the automatic calculation of the performance measures identified to evaluate the models. The evaluation of the models illustrates how the performance of the warehouse's sale is negatively affected by denial of service attack through preventing some or all customers' orders from being fulfilled. The resultant delay on selling perishable products would result on products being discarded.

In the area of Markovian quantitative modelling, compositional model specification techniques such as Stochastic Process Algebra are widely used. However, exploiting a model's compositional structure for efficient analysis is still a difficult problem and mostly limited to special cases. This paper addresses some important issues in the area of compositional model checking of Markovian models for models with Boucherie-type product form. It closes a long-standing gap concerning the question whether compositional model checking of so-called global time-unbounded Until formulas is possible. The answer to this turns out to be negative. The paper then turns to the area of model repair, i.e. the question of how to fix a model in case it violates a given requirement. Here another general result and a useful proposition for compositional model repair are provided.

In this paper we present a modeling approach suitable for practical evaluation of the delays that may affect security monitoring systems in (multitenant) cloud based architecture, and in general to support professionals in planning and evaluating relevant parameters in dealing with new designs or migration projects. The approach is based on modularity and multiformalism techniques to manage complexity and guide designers in an incremental process, to help transferring technical knowledge into modeling practice and to help easing the use of simulation. We present a case study based on a real experience, triggered by a new legal requirement that Italian Public Administration should comply about their datacenters.

Bisimulation is a concept that captures behavioural equivalence of states in a transition system. In [Linan Chen, Florence Clerc, and Prakash Panangaden, Bisimulation for feller-dynkin processes, in: Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science 347 (2019) 45–63.], we proposed two equivalent definitions of bisimulation on continuous-time stochastic processes where the evolution is a flow through time. In the present paper, we develop the theory further: we introduce different concepts that correspond to different behavioural equivalences and compare them to bisimulation. In particular, we study the relation between bisimulation and symmetry groups of the dynamics. We also provide a game interpretation for two of the behavioural equivalences. We then compare those notions to their discrete-time analogues.

Algebras can be used to interpret the behaviour of effectful programs. In particular, we use Eilenberg-Moore algebras given over a complete lattices of truth values, which specify answers to queries about programs. The algebras can be used to formulate a quantitative logic of behavioural properties, specifying a congruent notion of program equivalence coinciding with a notion of applicative bisimilarity. Many combinations of effects can be interpreted using these algebras. In this paper, we specify a method of generically combining effects and the algebras used to interpret them. At the core of this method is the tensor of complete lattices, which combines the carrier sets of the algebras. We show that this tensor preserves complete distributivity of complete lattices. Moreover, the universal properties of this tensor can then be used to properly combine the Eilenberg-Moore algebras. We will apply this method to combine the effects of probability, global store, cost, nondeterminism, and error effects. We will then compare this method of combining effects with the more traditional method of combining equational theories using interaction laws.

Kozen introduced probabilistic propositional dynamic logic (PPDL) in 1985 as a compositional framework to reason about probabilistic programs. In this paper we study expressiveness for PPDL and provide a series of results analogues to the classical Hennessy-Milner theorem for modal logic. First, we show that PPDL charaterises probabilistic trace equivalence of probabilistic automata (with outputs). Second, we show that PPDL can be mildly extended to yield a characterisation of probabilistic state bisimulation for PPDL models. Third, we provide a different extension of PPDL, this time characterising probabilistic event bisimulation.

Parametrized fixed points are of particular interest to denotational semantics and are often given by “dagger operations” [Stephen L. Bloom and Zoltan Esik, Fixed-Point Operations on ccc's. Part I, Theoretical Computer Science (ISSN 0304-3975) 155 (1996), 1–38, https://doi.org/10.1016/0304-3975(95)00010-0 ; Stephen L. Bloom and Zoltan Esik, Iteration Theories. The Equational Logic of Iterative Processes, in: EATCS Monographs on Theoretical Computer Science, Springer-Verlag Berlin Heidelberg, ISBN 978-3-642-78034-9, 1993, xv+630 pp., https://doi.org/10.1007/978-3-642-78034-9 ; Stephen L. Bloom and Zoltan Esik, Some Equational Laws of Initiality in 2CCC's, International Journal of Foundations of Computer Science 6 (1995) 95–118, https://doi.org/10.1142/S0129054195000081 .]. Dagger operations that satisfy the Conway identities [Stephen L. Bloom and Zoltan Esik, Fixed-Point Operations on ccc's. Part I, Theoretical Computer Science (ISSN 0304-3975) 155 (1996), 1–38, doi: https://doi.org/10.1016/0304-3975(95)00010-0 .] are particularly useful, because these identities imply a large class of identities used in semantic reasoning. We generalize existing techniques to define dagger operations on ω-categories and on O-categories. These operations enjoy a 2-categorical structure that implies the Conway identities. We illustrate these operators by considering applications to the semantics of session-typed languages.

We consider a pre-existing formalization in Constructive Type Theory of the pure Lambda Calculus in its presentation in first order syntax with only one sort of names and alpha-conversion based upon multiple substitution, as well as of the system of assignment of simple types to terms. On top of it, we formalize a slick proof of strong normalization given by Joachimski and Matthes whose main lemma proceeds by complete induction on types and subordinate induction on a characterization of the strongly normalizing terms which is in turn proven sound with respect to their direct definition as the accessible part of the relation of one-step beta reduction. The proof of strong normalization itself is thereby allowed to consist just of a direct induction on the type system. The whole development has been machine-checked using the system Agda. We assess merits and drawbacks of the approach.

Multiparty interactions are common place in today's distributed systems. An agent usually communicates, in a single session, with other agents to accomplish a given task. Take for instance an online transaction including the vendor, the client, the credit card system and the bank. When specifying this kind of system, we probably observe a single transaction including several (binary) communications leading to changes in the state of all the involved agents. Multiway synchronization process calculi, that move from a binary to a multiparty synchronization discipline, have been proposed to formally study the behavior of those systems. However, adopting models such as Bodei, Brodo, and Bruni's Core Network Algebra (CNA), where the number of participants in an interaction is not fixed a priori, leads to an exponential blow-up in the number of states/behaviors that can be observed from the system. In this paper we explore mechanisms to tackle this problem. We extend CNA with constraints that declaratively allow the modeler to restrict the interaction that should actually happen. Our extended process algebra, called CCNA, finds application in balancing the interactions in a concurrent system, leading to a simple, deadlock-free and fair solution for the Dinning Philosopher problem. Our definition of constraints is general enough and it offers the possibility of accumulating costs in a multiparty negotiation. Hence, only computations respecting the thresholds imposed by the modeler are observed. We use this machinery to neatly model a Service Level Agreement protocol. We develop the theory of CCNA including its operational semantics and a behavioral equivalence that we prove to be a congruence. We also propose a prototypical implementation that allows us to verify, automatically, some of the systems explored in the paper.

Rule-based languages, such as Kappa and BNGL, allow for the description of very combinatorial models of interactions between proteins. A huge (when not infinite) number of different kinds of bio-molecular compounds may arise due to proteins with multiple binding and phosphorylation sites. Knowing beforehand whether a model may involve an infinite number of different kinds of bio-molecular compounds is crucial for the modeller. On the first hand, having an infinite number of kinds of bio-molecular compounds is sometimes a hint for modelling flaws: forgetting to specify the conflicts among binding rules is a common mistake. On the second hand, it impacts the choice of the semantics for the models (among stochastic, differential, hybrid). In this paper, we introduce a data-structure to abstract the potential unbounded polymers that may be formed in a rule-based model. This data-structure is a graph, the nodes and the edges of which are labelled with patterns. By construction, every potentially unbounded polymer is associated to at least one cycle in that graph. This data-structure has two main advantages. Firstly, as opposed to site-graphs, one can reason about cycles without enumerating them (by the means of Tarjan's algorithm for detecting strongly connected components). Secondly, this data-structures may be combined easily with information coming from additional reachability analysis: the edges that are labelled with an overlap that is proved unreachable in the model may be safely discarded.

The analysis of information flow is a popular technique for ensuring the confidentiality of data. It is in this context that confidentiality policies arise for giving guarantees that private data cannot be inferred by the inspection of public data. One of those policies is non-interference, a semantic condition that ensures the absence of illicit information flow during program execution by not allowing to distinguish the results of two computations when they only vary in their confidential inputs. A remarkable feature of non-interference is that it can be enforced statically by the definition of information flow type systems. In those type systems, if a program type-checks, then it means that it meets the security policy. In this paper we focus on the preservation of non-interference through program translation. Concretely, we formalize the proof of security preservation of Hunt and Sands' translation that transforms high-level While programs typable in a flow-sensitive type system into equivalent high-level programs typable in a flow-insensitive type system. Our formalization is performed in the dependently-typed language Agda. We use the expressive power of Agda's type system to encode the security type systems at the type level. A particular aspect of our formalization is that it follows a fully internalist approach where we decorate the type of the abstract syntax with security type information in order to obtain the representation of well-typed (i.e secure) programs. A benefit of this approach is that it allows us to directly express the property of security preservation in the type of the translation relation. In this manner, apart from inherently expressing the transformation of programs, the translation relation also stands for an inductive proof of security preservation.

Regression Test Selection (RTS) algorithms select which tests to rerun on revised code, reducing the time required to check for newly introduced errors. An RTS algorithm is considered safe if and only if all deselected tests would have unchanged results. In this paper, we present a formal proof of safety of an RTS algorithm based on that used by Ekstazi [Gligoric, M., L. Eloussi and D. Marinov, Practical regression test selection with dynamic file dependencies, in: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015 (2015), p. 211–222. URL https://doi.org/10.1145/2771783.2771784 ], a Java library for regression testing. Ekstazi's algorithm adds print statements to JVM code in order to collect the names of classes used by a test during its execution on a program. When the program is changed, tests are only rerun if a class they used changed. The main insight in their algorithm is that not all uses of classes must be noted, as many necessarily require previous uses, such as when using an object previously created. The algorithm we formally define and prove safe here uses an instrumented semantics to collect touched classes in an even smaller set of locations. We identify problems with Ekstazi's current collection location set that make it not safe, then present a modified set that will make it equivalent to our safe set. The theorems given in this paper have been formalized in the theorem prover Isabelle over JinjaDCI [Mansky, S. and E. L. Gunter, Dynamic class initialization semantics: A jinja extension, in: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019 (2019), p. 209–221. URL https://doi.org/10.1145/3293880.3294104 ], a semantics for a subset of Java and JVM including dynamic class initialization and static field and methods. We instrumented JinjaDCI's JVM semantics by giving a general definition for Collection Semantics, small-step semantics instrumented to collect information during execution. We also give a formal general definition of RTS algorithms, including a definition of safety.

Rational McNaughton functions may be implicitly represented by logical formulas in Łukasiewicz Infinitely-valued Logic by constraining the set of valuations to the ones that satisfy some specific formulas. This work investigates this implicit representation called representation modulo satisfiability and describes a polynomial algorithm that builds it — the representative formula and the constraining ones — for a given rational McNaughton function.

APUs (Accelerated Processing Units) are widely available in personal computers as low-cost processors that have a CPU and an integrated GPU for displaying graphics, in the same die. Using a ray tracing algorithm as a computationally intensive workload and taking advantage of the APU specific characteristics, we compare the performance of this SoC against CPU and GPU solutions in the same price range.

This paper presents an architecture for a parallel programming environment designed to assist the process of writing parallel programs. The proposed architecture allows the integration of several tools such as parallel programming skeletons and parallelizing compilers, among others. On the one hand, parallel programming skeletons simplify the design of parallel algorithms. On the other hand, parallelizing compilers rely on compiler capabilities to translate sequential programs into ones capable of using multiple processing units (CPU/GPU) found in personal computers (PCs). The technological solution presented in this work follows a microservices-oriented approach. This approach eases the integration of new parallel programming tools in the existing deployment through well-known protocols and existing services. We show how the aforementioned parallel programming tools were integrated to support the coding and parallelization of a general purpose cellular automata. Since the parallelization rely on the capabilities underlying to each tool, the focus of this work is not to deal with an efficient cellular automata parallelization. Instead, a promising microservice approach to the development of an extensible and scalable parallel programming environment is presented.

The Robust Transform based on the Weighted Median operator algorithm calculates the transform of a signal when it has been exposed to impulsive noise. Since this algorithm demands very long execution time, it is not useful for real time signal processing systems. In this context, this work presents several strategies to improve its performance, such as the reduction of redundant calculations, optimization in the memory access, and a multithreads version of the algorithm. Besides, the original estimation method is modified to decrease even more the average execution time, keeping the quality level of the numeric results. The experimental results show a 30% performance improvement by reducing redundant calculations and optimizing the memory access, without making modifications to the estimation method and without using multi-threaded processing; 93% performance improvement by introducing modifications to the estimation method; and 97% performance improvement by incorporating the multi-threaded processing.

A bracket abstraction is a syntactic operator to abstract variables in combinatory logic. There are different algorithms for different combinator systems. In this paper we present a recursive algorithm scheme, which generates a family of brackets abstractions, in which all the bracket abstractions referenced here are found. In addition, theorems with certain hypotheses are enunciated about the scheme, which state that the resulting abstraction operators, has one property or another. Thus forming a criteria for designing bracket abstractions that comply with a given property.

Several histogram equalization methods focus on enhancing the contrast as one of their main objectives, but usually without considering the details of the input image. Other methods seek to keep the brightness while improving the contrast, causing distortion. Among the multi-objective algorithms, the classical optimization (a priori) techniques are commonly used given their simplicity. One of the most representative method is the weighted sum of metrics used to enhance the contrast of an image. These type of techniques, beside just returning a single image, have problems related to the weight assignment for each selected metric. To avoid the pitfalls of the algorithms just mentioned, we propose a new method called MOPHE (Multi-Objective Pareto Histogram Equalization) which is based on Multi-objective Particle Swarm Optimization (MOPSO) approach combining different metrics in a posteriori selection criteria context. The goal of this method is three-fold: (1) improve the contrast (2) without losing important details, (3) avoiding an excessive distortion. MOPHE, is a pure multi-objective optimization algorithm, consequently a set of trade-off optimal solutions are generated, thus providing alternative solutions to the decision-maker, allowing the selection of one or more resulting images, depending on the application needs. Experimental results indicate that MOPHE is a promising approach, as it calculates a set of trade-off optimal solutions that are better than the results obtained from representative algorithms from the state-of-the-art regarding visual quality and metrics measurement.

Center-based clustering is a set of clustering problems that require finding a single element, a center, to represent an entire cluster. The algorithms that solve this type of problems are very efficient for clustering large and high-dimensional datasets. In this paper, we propose a similar heuristic used in Lloyd's algorithm to approximately solve (EMAX algorithm) a more robust variation of the k-means problem, namely the EMAX problem. Also, a new center-based clustering algorithm (SSO-C) is proposed, which is based on a swarm intelligence technique called Social Spider Optimization. This algorithm minimizes a multi-objective optimization function defined as a weighted combination of the objective functions of the k-means and EMAX problems. Also, an approximation algorithm for the discrete k-center problem is used as a local search strategy for initializing the population. Results of the experiments showed that SSO-C algorithm is suitable for finding maximum best values, however EMAX algorithm is better in finding median and mean values.

Populational Announcement Logic (PPAL), is a variant of the standard Public Announcement Logic (PAL) with a fuzzy-inspired semantics, where instead of specific agents we have populations and groups. The semantics and the announcement logic are defined, and an example is provided. We show validities analogous to PAL axioms and their proofs, and also provide a proof of decidability. We briefly talk about model checking and compare the framework against probabilistic logic. We conclude that the main advantage of PPAL over PAL is the flexibility to work with previously defined agents.

Probabilistic programming is an increasingly popular formalism for modeling randomness and uncertainty. Designing semantic models for probabilistic programs has been extensively studied, but is technically challenging. Particular complications arise when trying to account for (i) unstructured control-flow, a natural feature in low-level imperative programs; (ii) general recursion, an extensively used programming paradigm; and (iii) nondeterminism, which is often used to represent adversarial actions in probabilistic models, and to support refinement-based development. This paper presents a denotational-semantics framework that supports the three features mentioned above, while allowing nondeterminism to be handled in different ways. To support both probabilistic choice and nondeterministic choice, the semantics is given over control-flow hyper-graphs. The semantics follows an algebraic approach: it can be instantiated in different ways as long as certain algebraic properties hold. In particular, the semantics can be instantiated to support nondeterminism among either program states or state transformers. We develop a new formalization of nondeterminism based on powerdomains over sub-probability kernels. Semantic objects in the powerdomain enjoy a notion we call generalized convexity, which is a generalization of convexity. As an application, the paper sketches an algebraic framework for static analysis of probabilistic programs, which has been proposed in a companion paper.

In flowchart languages, predicates play an interesting double role. In the textual representation, they are often presented as conditions, i.e., expressions which are easily combined with other conditions (often via Boolean combinators) to form new conditions, though they only play a supporting role in aiding branching statements choose a branch to follow. On the other hand, in the graphical representation they are typically presented as decisions, intrinsically capable of directing control flow yet mostly oblivious to Boolean combination. While categorical treatments of flowchart languages are abundant, none of them provide a treatment of this dual nature of predicates. In the present paper, we argue that extensive restriction categories are precisely categories that capture such a condition/decision duality, by means of morphisms which, coincidentally, are also called decisions. Further, we show that having these categorical decisions amounts to having an internal logic: Analogous to how subobjects of an object in a topos form a Heyting algebra, we show that decisions on an object in an extensive restriction category form a De Morgan quasilattice, the algebraic structure associated with the (three-valued) weak Kleene logic $\mathbf{K}^w_3$. Full classical propositional logic can be recovered by restricting to total decisions, yielding extensive categories in the usual sense, and confirming (from a different direction) a result from effectus theory that predicates on objects in extensive categories form Boolean algebras. As an application, since (categorical) decisions are partial isomorphisms, this approach provides naturally reversible models of classical propositional logic and weak Kleene logic., 19 pages, including 6 page appendix of proofs. Accepted for MFPS XXXV

This article studies (multilayer perceptron) neural networks with an emphasis on the transformations involved — both forward and backward — in order to develop a semantic/logical perspective that is in line with standard program semantics. The common two-pass neural network training algorithms make this viewpoint particularly fitting. In the forward direction, neural networks act as state transformers, using Kleisli composition for the multiset monad — for the linear parts of network layers. In the reverse direction, however, neural networks change losses of outputs to losses of inputs, thereby acting like a (real-valued) predicate transformer. In this way, backpropagation is functorial by construction, as shown in other works recently. We illustrate this perspective by training a simple instance of a neural network.

It is commonly understood that Countable Choice holds constructively due to the underlying computational nature of constructivism. However, in this paper we demonstrate that invoking different notions of computation result in radically different behaviors regarding Countable Choice. In particular, we illustrate that, although deterministic computation guarantees Countable Choice, non-deterministic computation can negate Countable Choice. We then further show that using stateful computation can restore Countable Choice even in the presence of non-determinism. This finding suggests that much of the modern discourse of constructivism assumes a deterministic underlying computational system, despite non-determinism being a fundamental aspect of modern-day computation.

This paper extends the results of Hermida's thesis about logical predicates to more general logical relations and a wider collection of types. The extension of type constructors from types to logical relations is derived from an interpretation of those constructors on a model of predicate logic. This is then further extended to n-ary relations by pullback. Hermida's theory shows how right adjoints in the category of fibrations are composed from a combination of Cartesian lifting and a local adjunction. This result is generalised to make it more applicable to left adjoints, and then shown to be stable under pullback, deriving an account of n-ary relations from standard predicate logic. A brief discussion of lifting monads to predicates includes the existence of an initial such lifting, generalising existing results.

This work adapts a formalisation in Coq of a nominal C-unification algorithm to include “protected variables” that cannot be instantiated during the unification process. By introducing protected variables we are able to reuse the C-unification algorithm to solve nominal C-matching (as well as equality check) problems. From the algorithmic point of view having this extension would be enough to adapt the C-unification algorithm for dealing with equational check as well as with C-matching problems, but the resulting algorithms would not be formally checked by simple reuse of the original formalisation. This paper describes the additional effort necessary in order to adapt the specification and reuse previous formalisations.

The Bi-objective Spanning Tree (BiST) is an NP-hard extension of the Minimum Spanning Tree (MST) problem. The BiST models situations in which two conflicting objectives need to be optimized simultaneously. The BiST has been studied in the literature and several heuristic algorithms were proposed for it, most of them evolutionary techniques. The transgenetic algorithms are among these evolutionary techniques which were successfully applied to the BiST. However, a priori defined parameters can limit the search mechanisms used within the algorithm. In this study, we propose a new transgenetic algorithm for the BiST in which the decision about the search mechanisms used along its execution is automatically made. An analysis of the results of computational experiments carried on 165 benchmark instances showed that the algorithm proposed in this study produces good approximation sets concerning two different quality indicators.

Coloring problems in graphs have been used to model a wide range of real applications. In particular, the List Coloring Problem generalizes the well-known Graph Coloring Problem for which many exact algorithms have been developed. In this work, we present a Branch-and-Price algorithm for the weighted version of the List Coloring Problem, based on the one developed by Mehrotra and Trick (1996) for the Graph Coloring Problem. This version considers non-negative weights associated to each color and it is required to assign a color to each vertex from predetermined lists in such a way the sum of weights of the assigned colors is minimum. Computational experiments show the good performance of our approach, being able to comfortably solve instances whose graphs have up to seventy vertices. These experiences also bring out that the hardness of the instances of the List Coloring Problem does not seem to depend only on quantitative parameters such as the size of the graph, its density, and the size of list of colors, but also on the distribution of colors present in the lists.

In this paper, we consider a coloring as a function that assigns a color to a vertex, regardless of the color of its neighbors. The Convex Recoloring Problem finds the minimum number of recolored vertices needed to turn a coloring convex, that is, every set formed by all the vertices with the same color induces a connected subgraph. The problem is most commonly studied considering trees due to its origins in the study of phylogenetic trees, but in this paper, we focus on general graphs and propose a GRASP heuristic to solve the problem. We present computational experiments for our heuristic and compare it to an Integer Linear Programming model from the literature. In these experiments, the GRASP algorithm recolored a similar number of vertices than the model from the literature, and used considerably less time. We also introduce a set of benchmark instances for the problem.

Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma for Context-Free Languages states a property that is valid for all context-free languages, which makes it a tool for showing the existence of non-context-free languages. This paper presents a formalization, extending the previously formalized Lemma, of the fact that several well-known languages are not context-free. Moreover, we build on those results to construct a formal proof of the well-known property that context-free languages are not closed under intersection. All the formalization has been mechanized in the Coq proof assistant., (undefined)

Abstract Dialectical Frameworks ( adf s) are generalizations of Dung's abstract argumentation frameworks ( af s) where each argument has an associated acceptance condition expressed by a boolean formula. The resulting extension is robust enough not only to model the attack relation original to af s, but also others types of dependencies and interactions between arguments. A recent development in adf s proposed an alternative formalization involving three-valued acceptance conditions, connecting the original definitions of adf s to the concept of three-valued argument labellings, a core concept in computational argumentation literature. In this paper, we revise some of the main semantics defined under this three-valued approach and prove our definitions hold equivalence to well-known semantics of af s.

Given a d-dimensional array, the maximum subarray problem consists in finding an axis-parallel slice of the array maximizing the sum of its entries. In this work we start a polyhedral study of a natural integer programming formulation for this problem when d = 2. Such an exploration is motivated by the need of solving large-scale instances of the rectilinear picture compression problem (RPC), a problem which arises in different scenarios. The obtained results can be useful to solve the column generation phase of a branch and price approach for RPC, a technique that applies naturally to this problem. We thus define the 2D subarray polytope, explore conditions ensuring the validity of linear inequalities, and provide several families of facet-inducing inequalities.

Virtual avatars/characters are essential in the interaction with virtual environments and 3D video games. While these avatars can be controlled by a bot or a human, they need a suitable model that allows emotion representation regardless of what or who is controlling them, since it increases the interaction and immersion. Provide facial expressions to any avatar require an animation process to emulate a particular gesture or emotion before to include it in a virtual environment. This process is specific to every single facial expression required in the avatar. This paper presents an initial approximation to contribute to the solve this problem with a workflow to apply a well-known parameterized face model called Candide. The proposal aims to adapt Candide into any avatar previously modeled through automatic morphological adjustment and texture mapping. This work includes the application of this workflow into six characters licensed under the Creative Commons copyright. We also present examples of facial emotion animation, as well as subjective assessment by five experts in audiovisual and animation production.

GamECAR aims to develop a highly innovative and interactive Serious Games platform that will empower and guide users to adopt an eco-friendly driving style. This will be achieved, without distracting them from safe driving, through a multidisciplinary approach aiming at the development of a user friendly, unobtrusive multi-player gaming environment, where the users will not only play collaboratively/competitively using their mobile device but also use the car itself and their own bodies, thus turning eco-driving into an immersive and highly motivating experience. The sensing infrastructure of GamECAR will acquire data related to driving from an OBD sensor that will capture a complex set of parameters related to eco-driving, and will also sense environmental and physiological parameters of the driver, so as to better position the state of the system (car) in context (environment, user). The GamECAR system will be quantified and evaluated in test campaigns with drivers in three different sites that will serve system development and will also demonstrate usefulness and exploitation potential.

A significant component in computer-aided medical diagnosis is the automatic detection of lung abnormalities from digital chest X-rays; thus it constitutes a vital first step in radiologic image analysis. During the last decades, the rapid advances of digital technology and chest radiography have ultimately led to the development of large repositories with labeled and unlabeled images. Semi-supervised learning algorithms have become a hot topic of research, exploiting the explicit classification information of labeled images with the knowledge hidden in the unlabeled images. In the present work, we propose a new semi-supervised learning algorithm for the classification of lung abnormalities from X-rays based on an ensemble philosophy. The efficacy of the presented algorithm is demonstrated by numerical experiments, illustrating that reliable prediction models could be developed by incorporating ensemble methodologies in the semi-supervised framework.

Problem partitioning strategies such as sequential covering are commonly used in rule learning algorithms, such that the task of finding a complete rule base is reduced to a sequence of subproblems. In this scenario, each solution to a subproblem consists of adding a single rule to the entire set. In this paper, we propose an alternative for rule learning based on the use of an adaptive formalism whose behavior is determined by a dynamic set of rules. Preliminary results yield a compact yet significantly comprehensible rule set, as well as an efficient model representation, from raw data using adaptive techniques. To this end, we include further discussions regarding features and enhancements to be contemplated in future works.

The concept of computable functions (as developed by Godel, Church, Turing, and Kleene in the 1930's) has been extensively studied, leading to the modern subject of recursive function theory. However recent work by category theorists has led to a more conceptual and abstract foundation of computability theory—Turing categories. A Turing category models the notion of partial map as well as recursive computation, using methods of categorical algebra to formalize these concepts. The goal of this work is to provide a formal framework for analyzing this categorical model of computation. We use the Coq Proof Assistant, which implements the Calculus of (co)Inductive Constructions (CIC), and we build on an existing Coq library for general category theory. We focus on both formalizing Turing categories and on building a general framework in the form of a well-structured Coq library that can be further extended. We begin by formalizing definitions, propositions, and proofs pertaining to Turing categories, and then instantiate the more general Turing category formalism with a CIC description of the category which explicitly models the language of partial recursive functions.

Starting from works aimed at extending the Curry-Howard correspondence to process calculi through linear logic, we give another Curry-Howard counterpart for Milner's Calculus of Communicating Systems (CCS) by taking Ludics as the target system. Indeed interaction, Ludics' dynamic, allows to fully represent both the non-determinism and non-confluence of the calculus. We give an interpretation of CCS processes into carefully defined behaviours of Ludics using a new construction, called directed behaviour, that allows controlled interaction paths by using pruned designs. We characterize the execution of processes as interaction on behaviours, by implicitly representing the causal order and conflict relation of event structures. As a direct consequence, we are also able to interpret deadlocked processes, and identify deadlock-free ones.

In this article we continue the work started in [Ernesto Copello, Alvaro Tasistro, Nora Szasz, Ana Bove, and Maribel Fernandez. Alpha-structural induction and recursion for the λ-calculus in constructive type theory. Electronic Notes in Theoretical Computer Science, 323:109–124, 2016], deriving in Constructive Type Theory new induction principles for the λ-calculus, using (the historical) first order syntax with only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. The principles provide a flexible framework for mimicking pen-and-paper proofs within the rigorous formal setting of a proof assistant. We here report on one successful application, namely a complete proof of the Church-Rosser Theorem. The whole development has been machine-checked using the system Agda [Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007].

This paper proposes a discrete-time heterogeneous model to represent the interaction between the dynamic arrival process of multiple TCP sources and a bottleneck queue. It utilises a novel time-variant calculation approach for transient queueing models, which modifies the conventional steady-state method by no longer requiring the equilibrium assumption. The main contributions are: (1) The limitation of the conventional queueing method is analysed and the benefits of the proposed modification is demonstrated; (2) The proposed dynamic arrival process of multiple sources is illustrated, which interacts with the queueing process and statistically responds to the positive and negative congestion feedback; (3) The fidelity of the proposed model is extensively validated by the closely matched results from MATLAB numerical solutions and NS-2 discrete-event simulation experiments.

The design and development of quantum programming languages (QPLs) is an important and active area of quantum computing. This paper addresses the problem of developing a standard methodology for verifying a QPL against major quantum computing concepts. We propose a framework dedicated to the meta-level analysis of QPLs, in particular, functional quantum languages. To this aim, we choose the Hybrid system as the tool in which to build our framework. Hybrid is a logical framework that supports higher-order abstract syntax, on top of which we develop an intuitionistic linear specification logic used for reasoning about QPLs. We provide a formal proof of some important meta-theoretic properties of this logic, and in addition, showcase a number of examples that can be tackled under the proposed framework.

Multi-Agent Epistemic Logic has been investigated in Computer Science [Fagin, R., J. Halpern, Y. Moses and M. Vardi, “Reasoning about Knowledge,” MIT Press, USA, 1995] to represent and reason about agents or groups of agents knowledge and beliefs. Some extensions aimed to reasoning about knowledge and probabilities [Fagin, R. and J. Halpern, Reasoning about knowledge and probability, Journal of the ACM 41 (1994), pp. 340–367] and also with a fuzzy semantics have been proposed [Fitting, M., Many-valued modal logics, Fundam. Inform. 15 (1991), pp. 235–254; Maruyama, Y., Reasoning about fuzzy belief and common belief: With emphasis on incomparable beliefs, in: IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16–22, 2011, 2011, pp. 1008–1013]. This paper introduces a parametric method to build graded epistemic logics inspired in the systematic method to build Multi-valued Dynamic Logics introduced in [Madeira, A., R. Neves and M. A. Martins, An exercise on the generation of many-valued dynamic logics, J. Log. Algebr. Meth. Program. 85 (2016), pp. 1011–1037. URL http://dx.doi.org/10.1016/j.jlamp.2016.03.004 ; Madeira, A., R. Neves, M. A. Martins and L. S. Barbosa, A dynamic logic for every season, in: C. Braga and N. Marti-Oliet, editors, Formal Methods: Foundations and Applications – 17th Brazilian Symposium, SBMF 2014, Maceio, AL, Brazil, September 29-October 1, 2014. Proceedings, Lecture Notes in Computer Science 8941 (2014), pp. 130–145. URL http://dx.doi.org/10.1007/978-3-319-15075-8_9 ]. The parameter in both methods is the same: an action lattice [Kozen, D., On action algebras, Logic and Information Flow (1994), pp. 78–88]. This algebraic structure supports a generic space of agent knowledge operators, as choice, composition and closure (as a Kleene algebra), but also a proper truth space for possible non bivalent interpretation of the assertions (as a residuated lattice).

There are different algebraic structures that one can use to model notions of computation. The most well- known are monads, but lately, applicative functors have been gaining popularity. These two structures can be understood as instances of the unifying notion of monoid in a monoidal category. When dealing with non-determinism, it is usual to extend monads and applicative functors with additional structure. However, depending on the desired non-determinism, there are different options of interaction between the existing and the additional structure. This article studies one of those options, which is captured algebraically by dioids. We generalise dioids to dioid categories and show how dioids in such a category model non- determinism in monads and applicative functors. Moreover, we study the construction of free dioids in a programming context.

In this paper we present a series of theorems that allow to establish strategies for the calculation of invariant assertions, such as the Dijkstra's H k ( Post ) , or the weakest precondition of the loop. A criterion is also shown for calculating the termination condition of a loop. As in the integrals calculus, the strategies proposed here to perform the calculation of an invariant, will depend on the shape of the loop with which it is working, particularly will work with for-type loops with or without early termination due to a sentry. http://www.elsevier.com/locate/entcs .

In this work we study pebble automata. Those automata constitute an infinite hierarchy of discrete models of computation. The hierarchy begins at the level of finite state automata (0-pebble automata) and approaches the model of one-tape Turing machines. Thus, it can be argued that it is a complete hierarchy that covers, in a continuous way, all the models of automata that are important in the theory of computation. We investigate the use of this hierarchy as a narrative for the teaching of automata theory. We also investigate some fundamental questions concerning the power of pebble automata.

We study synchronization games on planar automata. We prove that recognizing the planar games that can be won by the synchronizer is a co-NP hard problem. We prove some additional results indicating that planar games are as hard as nonplanar games. Those results amount to show that planar automata are representative of the intricacies of automata synchronization.