Unified Representation of Twitter and Online News Using Graph and Entities

To improve consumer engagement and satisfaction, online news services employ strategies for personalizing and recommending articles to their users based on their interests. In addition to news agencies’ own digital platforms, they also leverage social media to reach out to a broad user base. These engagement efforts are often disconnected with each other, but present a compelling opportunity to incorporate engagement data from social media to inform their digital news platform and vice-versa, leading to a more personalized experience for users. While this idea seems intuitive, there are several challenges due to the disparate nature of the two sources. In this paper, we propose a model to build a generalized graph of news articles and tweets that can be used for different downstream tasks such as identifying sentiment, trending topics, and misinformation, as well as sharing relevant articles on social media in a timely fashion. We evaluate our framework on a downstream task of identifying related pairs of news articles and tweets with promising results. The content unification problem addressed by our model is not unique to the domain of news, and thus can be applicable to other problems linking different content platforms.

Extensions of unification modulo ACUI

The theory ACUI of an associative, commutative, and idempotent binary function symbol + with unit 0 was one of the first equational theories for which the complexity of testing solvability of unification problems was investigated in detail. In this paper, we investigate two extensions of ACUI. On one hand, we consider approximate ACUI-unification, where we use appropriate measures to express how close a substitution is to being a unifier. On the other hand, we extend ACUI-unification to ACUIG-unification, that is, unification in equational theories that are obtained from ACUI by adding a finite set G of ground identities. Finally, we combine the two extensions, that is, consider approximate ACUI-unification. For all cases we are able to determine the exact worst-case complexity of the unification problem.

A framework for improving error messages in dependently-typed languages

Dependently-typed programming languages provide a powerful tool for establishing code correctness. However, it can be hard for newcomers to learn how to employ the advanced type system of such languages effectively. For simply-typed languages, several techniques have been devised to generate helpful error messages and suggestions for the programmer. We adapt these techniques to dependently-typed languages, to facilitate their more widespread adoption. In particular, we modify a higher-order unification algorithm that is used to resolve and type-check implicit arguments. We augment this algorithm with replay graphs, allowing for a global heuristic analysis of a unification problem-set, error-tolerant typing, which allows type-checking to continue after errors are found, and counter-factual unification, which makes error messages less affected by the order in which types are checked. A formalization of our algorithm is presented with an outline of its correctness. We implement replay graphs, and compare the generated error messages to those from existing languages, highlighting the improvements we achieved.

Is it possible to unify sequential programs?

We introduce a first-order model of imperative sequential programs and set up formally the unification problem in this model: given a pair of programs π<sub>1</sub> and π<sub>2</sub> find a pair of substitutions (θ<sub>1</sub>,θ<sub>2</sub>) such that the instances π<sub>1</sub>θ<sub>1</sub> and π<sub>2</sub>θ<sub>2</sub> of these programs are equivalent, i.e. compute the same function. Since functional equivalence of programs is undecidable, we choose its decidable approximation --- a strong equivalence, --- which is well-known in theory of program schemata. Our main result is a polynomial time unification algorithm for sequential programs w.r.t. strong equivalence of programs.

Unranked Anti-Unification with Hedge and Context Variables

In this work we study anti-unification for unranked terms and hedges, permitting context and hedge variables.Hedges are sequences of unranked terms.The anti-unification problem of two hedges s and q is concerned with finding their generalization, a hedge g such that both s and q are instances of g under some substitutions.Context variables are used to abstract vertical differences in the input hedges,and hedge variables are used to abstract horizontal differences.A rule based system in Huet's style will be presented, which computes a set ofgeneralizations of input hedges and records all the differences.The computed generalizations are least general among a certain class of generalizations.

Anti-Unification: Algorithms and Applications

The anti-unification problem of two terms t<sub>1</sub> and t<sub>2</sub> is concerned with finding a term t which generalizes both t<sub>1</sub> and t<sub>2</sub>. That is, the input terms should be substitution instances of the generalization term. Interesting generalizations are the least general ones. The purpose of anti-unification algorithms is to compute such least general generalizations.Research on anti-unification has been initiated more than four decades ago, with the pioneering works by Gordon~D.~Plotkin and John~C.~Reynolds. Since then, a number of algorithms and their modifications have been developed, addressing the problem in first-order or higher-order languages, for syntactic or equational theories, over ranked or unranked alphabets, with or without sorts/types, etc. Anti-unification has found applications in machine learning, inductive logic programming, case-based reasoning, analogy making, symbolic mathematical computing, software maintenance, program analysis, synthesis, transformation, and verification. Some of these algorithms and applications will be reviewed in the talk. We will also consider recent developments in unranked and higher-order generalization computation.

Analysis of Service Compatibility

In this chapter, the authors apply type-theoretic techniques to the service description and composition verification. A flexible type system is introduced for modeling instances and mappings of semi-structured data, and is demonstrated to be effective in modeling a wide range of data services, ranging from relational database queries to web services for XML. Type-theoretic analysis and verification are then reduced to the problem of type unification. Some (in)tractability results of the unification problem and the expressiveness of their proposed type system are presented in this chapter. Finally, the auhtors construct a complete unification algorithm which runs in EXP-TIME in the worst case, but runs in polynomial time for a large family of unification problems rising from practical type analysis of service compositions.