bluuebunny/crossref_metadata_2025 huggingface dataset:
A Calculus of Circular Proofs and its Categorical Semantics
Authors: Santocanale Luigi
Published: February 2016

We present a calculus of proofs, the intended models of which
are categories with finite products and coproducts, initial algebras
and final coalgebras of functors that are recursively constructible
out of these operations, that is, mu-bicomplete categories. The
calculus satisfies the cut elimination and its main characteristic is
that the underlying graph of a proof is allowed to contain a
certain amount of cycles. To each proof of the calculus we associate
a system of equations which has a meaning in every mu-bicomplete
category. We prove that this system admits always a unique
solution, and by means of this theorem we define the semantics of
the calculus.

Keywords: Initial algebras, final coalgebras. Fixed point calculi, mu-calculi.
Bicompletion of categories. Models of interactive computation.
The Equational Theory of Fixed Points with Applications to Generalized Language Theory
Authors: Ésik Zoltán
Published: February 2016

We review the rudiments of the equational logic of (least) fixed points and provide some of its applications for axiomatization problems with respect to regular languages, tree languages, and synchronization trees.
Defunctionalization at Work
Authors: Danvy Olivier , Nielsen Lasse R.
Published: February 2016

We study practical applications of Reynolds's defunctionalization technique, which is a whole-program transformation from higher-order to first-order functional programs. This study leads us to discover new connections between seemingly unrelated higher-order and first-order specifications and their correctness proofs. We thus perceive defunctionalization both as a springboard and as a bridge: as a springboard for discovering new connections between the first-order world and the higher-order world; and as a bridge for transferring existing results between first-order and higher-order settings.
Automata on Series-Parallel Biposets
Authors: Ésik Zoltán , Németh Zoltán L.
Published: February 2016

We provide the basics of a 2-dimensional theory of automata on series-parallel biposets. We define recognizable, regular and rational sets of series-parallel biposets and study their relationship. Moreover, we relate these classes to languages of series-parallel biposets definable in monadic second-order logic.
Cost Recurrences for DML Programs
Authors: Grobauer Bernd
Published: February 2016

A cost recurrence describes an upper bound for the running time of a program in terms of the size of its input. Finding cost recurrences is a frequent intermediate step in complexity analysis, and this step requires an abstraction from data to data size. In this article, we use information contained in dependent types to achieve such an abstraction: Dependent ML (DML), a conservative extension of ML, provides dependent types that can be used to associate data with size information, thus describing a possible abstraction. We systematically extract cost recurrences from first-order DML programs, guiding the abstraction from data to data size with information contained in DML type derivations.
A Selective CPS Transformation
Authors: Nielsen Lasse R.
Published: February 2016

The CPS transformation makes all functions continuation-passing, uniformly. Not all functions, however, need continuations: they only do if their evaluation includes computational effects. In this paper we focus on control operations, in particular ``call with current continuation'' and ``throw''. We characterize this involvement as a control effect and we present a selective CPS transformation that makes functions and expressions continuation-passing if they have a control effect, and that leaves the rest of the program in direct style. We formalize this selective CPS transformation with an operational semantics and a simulation theorem à la Plotkin.
Universal Hash Proofs and a Paradigm for Adaptive Chosen Ciphertext Secure Public-Key Encryption
Authors: Cramer Ronald , Shoup Victor
Published: February 2016

We present several new and fairly practical public-key encryption schemes and prove them secure against adaptive chosen ciphertext attack. One scheme is based on Paillier's Decision Composite Residuosity (DCR) assumption, while another is based in the classical Quadratic Residuosity (QR) assumption. The analysis is in the standard cryptographic model, i.e., the security of our schemes does not rely on the Random Oracle model.

We also introduce the notion of a universal hash proof system. Essentially, this is a special kind of non-interactive zero-knowledge proof system for an NP language. We do not show that universal hash proof systems exist for all NP languages, but we do show how to construct very efficient universal hash proof systems for a general class of group-theoretic language membership problems.

Given an efficient universal hash proof system for a language with certain natural cryptographic indistinguishability properties, we show how to construct an efficient public-key encryption schemes secure against adaptive chosen ciphertext attack in the standard model. Our construction only uses the universal hash proof system as a primitive: no other primitives are required, although even more efficient encryption schemes can be obtained by using hash functions with appropriate collision-resistance properties. We show how to construct efficient universal hash proof systems for languages related to the DCR and QR assumptions. From these we get corresponding public-key encryption schemes that are secure under these assumptions. We also show that the Cramer-Shoup encryption scheme (which up until now was the only practical encryption scheme that could be proved secure against adaptive chosen ciphertext attack under a reasonable assumption, namely, the Decision Diffie-Hellman assumption) is also a special case of our general theory.
There and Back Again
Authors: Danvy Olivier , Goldberg Mayer
Published: February 2016

We illustrate a variety of programming problems that seemingly require two separate list traversals, but that can be efficiently solved in one recursive descent, without any other auxiliary storage but what can be expected from a control stack. The idea is to perform the second traversal when returning from the first.

This programming technique yields new solutions to traditional problems. For example, given a list of length 2n or 2n+1, where n is unknown, we can detect whether this list is a palindrome in n+1 recursive calls and no heap allocation.
Efficient Guiding Towards Cost-Optimality in UPPAAL
Authors: Behrmann Gerd , Fehnker Ansgar , Hune Thomas S. , Larsen Kim G. , Pettersson Paul , Romijn Judi
Published: February 2016

In this paper we present an algorithm for efficiently computing
 the minimum cost of reaching a goal state in the model of Uniformly
Priced Timed Automata (UPTA). This model can be seen as a submodel
of the recently suggested model of linearly priced timed automata, which
extends timed automata with prices on both locations and transitions.
The presented algorithm is based on a symbolic semantics of UTPA, and
an efficient representation and operations based on difference bound
matrices. In analogy with Dijkstra's shortest path algorithm, we show that
the search order of the algorithm can be chosen such that the number of
symbolic states explored by the algorithm is optimal, in the sense that
the number of explored states can not be reduced by any other search
order based on the cost of states. We also present a number of techniques
inspired by branch-and-bound algorithms which can be used for limiting
the search space and for quickly finding near-optimal solutions.
The algorithm has been implemented in the verification tool Uppaal.
When applied on a number of experiments the presented techniques
reduced the explored state-space with up to 90%.
Rationally Additive Semirings
Authors: Ésik Zoltán , Kuich Werner
Published: February 2016

We define rationally additive semirings that are a generalization of (omega-)complete and (omega-)continuous semirings. We prove that every rationally additive semiring is an iteration semiring. Moreover, we characterize the semirings of rational power series with coefficients in N_infty, the semiring of natural numbers equipped with a top element, as the free rationally additive semirings.
Predicate Abstraction for Dense Real-Time Systems
Authors: Möller M. Oliver , Ruess Harald , Sorea Maria
Published: February 2016

We propose predicate abstraction as a means for verifying a rich class of safety and liveness properties for dense real-time systems. First, we define a restricted semantics of timed systems which is observationally equivalent to the standard semantics in that it validates the same set of mu-calculus formulas without a next-step operator. Then, we recast the model checking problem S |= phi for a timed automaton S and a mu-calculus formula phi in terms of predicate abstraction. Whenever a set of abstraction predicates forms a so-called basis, the resulting abstraction is strongly preserving in the sense that S validates phi iff the corresponding finite abstraction validates this formula phi. Now, the abstracted system can be checked using familiar mu-calculus model checking.

Like the region graph construction for timed automata, the predicate abstraction algorithm for timed automata usually is prohibitively expensive. In many cases it suffices to compute an approximation of a finite bisimulation by using only a subset of the basis of abstraction predicates. Starting with some coarse abstraction, we define a finite sequence of refined abstractions that converges to a strongly preserving abstraction. In each step, new abstraction predicates are selected nondeterministically from a finite basis. Counterexamples from failed mu-calculus model checking attempts can be used to heuristically choose a small set of new abstraction predicates for refining the abstraction.
Temporal Concurrent Constraint Programming: Applications and Behavior
Authors: Nielsen Mogens , Valencia Frank D.
Published: February 2016

The ntcc calculus is a model of non-deterministic temporal concurrent constraint programming. In this paper we study behavioral notions for this calculus. In the underlying computational model, concurrent constraint processes are executed in discrete time intervals. The behavioral notions studied reflect the reactive interactions between concurrent constraint processes and their environment, as well as internal interactions between individual processes. Relationships between the suggested notions are studied, and they are all proved to be decidable for a substantial fragment of the calculus. Furthermore, the expressive power of this fragment is illustrated by examples.
Linear Parametric Model Checking of Timed Automata
Authors: Hune Thomas S. , Romijn Judi , Stoelinga Mariëlle , Vaandrager Frits W.
Published: February 2016

We present an extension of the model checker Uppaal capable
 of synthesizing linear parameter constraints for the correctness of
parametric timed automata. The symbolic representation of the (parametric)
 state-space is shown to be correct. A second contribution of this
paper is the identification of a subclass of parametric timed automata
(L/U automata), for which the emptiness problem is decidable, contrary
to the full class where it is know to be undecidable. Also we present a
number of lemmas enabling the verification effort to be reduced for L/U
automata in some cases. We illustrate our approach by deriving linear
parameter constraints for a number of well-known case studies from the
literature (exhibiting a flaw in a published paper).
On Weak Markov's Principle
Authors: Kohlenbach Ulrich
Published: February 2016

We show that the so-called weak Markov's principle (WMP) which states that every pseudo-positive real number is positive is underivable in T^{omega}:= E-HA^{omega} + AC. Since T^{omega} allows to formalize (at least large parts of) Bishop's constructive mathematics this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics (which has been open for about 20 years). The underivability even holds if the ineffective schema of full comprehension (in all types) for negated formulas (in particular for $\exists$-free formulas) is added which allows to derive the law of excluded middle for such formulas.
A Simple CPS Transformation of Control-Flow Information
Authors: Damian Daniel , Danvy Olivier
Published: February 2016

We build on Danvy and Nielsen's first-order program transformation into continuation-passing style (CPS) to design a new CPS transformation of flow information that is simpler and more efficient than what has been presented in previous work. The key to simplicity and efficiency is that our CPS transformation constructs the flow information in one go, instead of first computing an intermediate result and then exploiting it to construct the flow information.

More precisely, we show how to compute control-flow information for CPS-transformed programs from control-flow information for direct-style programs and vice-versa. As a corollary, we confirm that CPS transformation has no effect on the control-flow information obtained by constraint-based control-flow analysis. The transformation has immediate applications in assessing the effect of the CPS transformation over other analyses such as, for instance, binding-time analysis.
Traveling Salesman Should not be Greedy: Domination Analysis of Greedy-Type Heuristics for the TSP
Authors: Gutin Gregory , Yeo Anders , Zverovich Alexey
Published: February 2016

Computational experiments show that the greedy algorithm (GR)
and the nearest neighbor algorithm (NN), popular choices for tour
construction heuristics, work at acceptable level for the Euclidean TSP,
but produce very poor results for the general Symmetric and Asymmetric
 TSP (STSP and ATSP). We prove that for every n >= 2 there
is an instance of ATSP (STSP) on n vertices for which GR finds the
worst tour. The same result holds for NN. We also analyze the repetitive
 NN (RNN) that starts NN from every vertex and chooses the best
tour obtained. We prove that, for the ATSP, RNN always produces
a tour, which is not worse than at least n/2 − 1 other tours, but for
some instance it finds a tour, which is not worse than at most n − 2
other tours, n >= 4. We also show that, for some instance of the STSP
on n >= 4 vertices, RNN produces a tour not worse than at most 2^(n−3) tours. These results are in sharp contrast to earlier results by G. Gutin and A. Yeo, and A. Punnen and S. Kabadi, who proved that, for the ATSP, there are tour construction heuristics, including some popular ones, that always build a tour not worse than at least (n − 2)! tours.

Keywords: TSP, domination analysis, greedy algorithm, nearest
neighbor algorithm
Checking for Open Bisimilarity in the pi-Calculus
Authors: Frendrup Ulrik , Jensen Jesper Nyholm
Published: February 2016

This paper deals with algorithmic checking of open bisimilarity in the pi-calculus. Most bisimulation checking algorithms are based on the partition refinement approach. Unfortunately the definition of open bisimulation does not permit us to use a partition refinement approach for open bisimulation checking directly, but in the paper 'A Partition Refinement Algorithm for the pi-Calculus' Marco Pistore and Davide Sangiorgi present an iterative method that makes it possible to check for open bisimilarity using partition refinement. We have implemented the algorithm presented by Marco Pistore and Davide Sangiorgi. Furthermore,
we have optimized this algorithm and implemented this optimized algorithm. The time-complexity of this algorithm is the same as the time-complexity for the first algorithm, but performance tests have shown that in many cases the running time of the optimized algorithm is shorter than the running time of the first algorithm. Our implementation of the optimized open bisimulation checker algorithm and a user interface have been integrated in a system called the OBC Workbench.The source code and a manual for it is available from http://www.cs.auc.dk/research/FS/ny/PR-pi/.
Uniform Asymptotic Regularity for Mann Iterates
Authors: Kohlenbach Ulrich
Published: February 2016

In a previous paper we obtained an effective quantitative analysis of a theorem due to Borwein, Reich and Shafrir on the asymptotic behavior of general Krasnoselski-Mann iterations for nonexpansive self-mappings of convex sets C in arbitrary normed spaces. We used this result to obtain a new strong uniform version of Ishikawa's theorem for bounded C . In this paper we give a qualitative improvement of our result in the unbounded case and prove the uniformity result for the bounded case under the weaker assumption that C contains a point x whose Krasnoselski-Mann iteration (x_n) is bounded.
We also consider more general iterations for which asymptotic regularity is known only for uniformly convex spaces (Groetsch). We give uniform effective bounds for (an extension of) Groetsch's theorem which generalize previous results by Kirk/Martinez-Yanez and the author.
A Simple Correctness Proof of the Direct-Style Transformation
Authors: Nielsen Lasse R.
Published: February 2016

We build on Danvy and Nielsen's first-order program transformation into continuation-passing style (CPS) to present a new correctness proof of the converse transformation, i.e., a one-pass transformation from CPS back to direct style. Previously published proofs were based on, e.g., a one-pass higher-order CPS transformation, and were complicated by having to reason about higher-order functions. In contrast, this work is based on a one-pass CPS transformation that is both compositional and first-order, and therefore the proof simply proceeds by structural induction on syntax.
On the Expressive Power of Concurrent Constraint Programming Languages
Authors: Nielsen Mogens , Palamidessi Catuscia , Valencia Frank D.
Published: February 2016

The tcc paradigm is a formalism for timed concurrent constraint programming. Several tcc languages differing in their way of expressing infinite behaviour have been proposed in the literature. In this paper we study the expressive power of some of these languages. In particular, we show that:(1)recursive procedures with parameters can be encoded into parameterless recursive procedures with dynamic scoping, and vice-versa.(2)replication can be encoded into parameterless recursive procedures with static scoping, and vice-versa.(3)the languages from (1) are strictly more expressive than the languages from (2).Furthermore, we show that behavioural equivalence is undecidable for the languages from (1), but decidable for the languages from (2). The undecidability result holds even if the process variables take values from a fixed finite domain.
Lambda-Lifting in Quadratic Time
Authors: Danvy Olivier , Schultz Ulrik P.
Published: February 2016

Lambda-lifting is a program transformation used in compilers and in partial evaluators and that operates in cubic time. In this article, we show how to reduce this complexity to quadratic time.

 Lambda-lifting transforms a block-structured program into a set of recursive equations, one for each local function in the source program. Each equation carries extra parameters to account for the free variables of the corresponding local function and of all its callees. It is the search for these extra parameters that yields the cubic factor in the traditional formulation of lambda-lifting, which is due to Johnsson. This search is carried out by a transitive closure.

Instead, we partition the call graph of the source program into strongly connected components, based on the simple observation that all functions in each component need the same extra parameters and thus a transitive closure is not needed. We therefore simplify the search for extra parameters by treating each strongly connected component instead of each function as a unit, thereby reducing the time complexity of lambda-lifting from O(n^3 log n) to O(n^2 log n), where n is the size of the program.

Since a lambda-filter can output programs of size O(n^2), we believe that our algorithm is close to optimal.

Superseded by (BRICS-RS-03-26 and) BRICS-RS-04-12.
A Symmetric Approach to Compilation and Decompilation
Authors: Ager Mads Sig , Danvy Olivier , Goldberg Mayer
Published: February 2016

Just as specializing a source interpreter can achieve compilation from a source language to a target language, we observe that specializing a target interpreter can achieve compilation from the target language to the source language. In both cases, the key issue is the choice of whether to perform an evaluation or to emit code that represents this evaluation.

We substantiate this observation by specializing two source interpreters and two target interpreters. We first consider a source language of arithmetic expressions and a target language for a stack machine, and then the lambda-calculus and the SECD-machine language. In each case, we prove that the target-to-source compiler is a left inverse of the source-to-target compiler, i.e., it is a decompiler.

In the context of partial evaluation, compilation by source-interpreter specialization is classically referred to as a Futamura projection. By symmetry, it seems logical to refer to decompilation by target-interpreter specialization as a Futamura embedding.
A Note on an Expressiveness Hierarchy for Multi-exit Iteration
Authors: Aceto Luca , Fokkink Willem Jan , Ingólfsdóttir Anna
Published: February 2016

Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of recursion equations of the form
X_1 = P_1 X_2 + Q_1

 X_n = P_n X_1 + Q_n

 where n is a positive integer, and the P_i and the Q_i are process terms. The addition of multi-exit iteration to Basic Process Algebra (BPA) yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star. This note offers an expressiveness hierarchy, modulo bisimulation equivalence, for the family of multi-exit iteration operators proposed by Bergstra, Bethke and Ponse.
Axiomatizing Omega and Omega-op Powers of Words
Authors: Bloom Stephen L. , Ésik Zoltán
Published: February 2016

In 1978, Courcelle asked for a complete set of axioms and rules for the equational theory of (discrete regular) words equipped with the operations of product, omega power and omega-op power. In this paper we find a simple set of equations and prove they are complete. Moreover, we show that the equational theory is decidable in polynomial time.
Chromatic Number in Time O(2.4023^n) Using Maximal Independent Sets
Authors: Byskov Jesper Makholm
Published: February 2016

In this paper we improve an algorithm by Eppstein (2001) for finding the chromatic number of a graph. We modify the algorithm slightly, and by using a bound on the number of maximal independent sets of size  k from our recent paper (2003), we prove that the running time is O(2.4023^n). Eppstein's algorithm runs in time O(2.4150^n). The space usage for both algorithms is O(2^n).
Greibach Normal Form in Algebraically Complete Semirings
Authors: Ésik Zoltán , Leiß Hans
Published: February 2016

We give inequational and equational axioms for semirings with a fixed-point operator and formally develop a fragment of the theory of context-free languages. In particular, we show that Greibach's normal form theorem depends only on a few equational properties of least pre-fixed-points in semirings, and elimination of chain- and deletion rules depend on their inequational properties (and the idempotency of addition). It follows that these normal form theorems also hold in non-continuous semirings having enough fixed-points.
HOPLA--A Higher-Order Process Language
Authors: Nygaard Mikkel , Winskel Glynn
Published: February 2016

A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a ``prefixed sum'', in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names.
A New One-Pass Transformation into Monadic Normal Form
Authors: Danvy Olivier
Published: February 2016

We present a translation from the call-by-value lambda-calculus to monadic normal forms that includes short-cut boolean evaluation. The translation is higher-order, operates in one pass, duplicates no code, generates no chains of thunks, and is properly tail recursive. It makes a crucial use of symbolic computation at translation time.
Optimal Black-Box Secret Sharing over Arbitrary Abelian Groups
Authors: Cramer Ronald , Fehr Serge
Published: February 2016

A black-box secret sharing scheme for the threshold access structure T_t,n is one which works over any finite Abelian group G. Briefly, such a scheme differs from an ordinary linear secret sharing scheme (over, say, a given finite field) in that distribution matrix and reconstruction vectors are defined over Z and are designed independently of the group G from which the secret and the shares are sampled. This means that perfect completeness and perfect privacy are guaranteed regardless of which group G is chosen. We define the black-box secret sharing problem as the problem of devising, for an arbitrary given T_t,n, a scheme with minimal expansion factor, i.e., where the length of the full vector of shares divided by the number of players, n, is minimal.
 Such schemes are relevant for instance in the context of distributed cryptosystems based on groups with secret or hard to compute group order. A recent example is secure general multi-party computation over black-box rings.
 In 1994 Desmedt and Frankel have proposed an elegant approach to the black-box secret sharing problem based in part on polynomial interpolation over cyclotomic number fields. For arbitrary given T_t,n with 0 < t < n-1, the expansion factor of their scheme is O(n). This is the best previous general approach to the problem.
 Using low degree integral extensions of Z over which there exists a pair of sufficiently large Vandermonde matrices with co-prime determinants, we construct, for arbitrary given T_t,n with 0 < t < n-1, a black-box secret sharing scheme with expansion factor O(log n), which we show is minimal.
One-Probe Search
Authors: Östlin Anna , Pagh Rasmus
Published: February 2016

We consider dictionaries that perform lookups by probing a single word of memory, knowing only the size of the data structure. We describe a randomized dictionary where a lookup returns the correct answer with probability 1 - epsilon, and otherwise returns "don't know''. The lookup procedure uses an expander graph to select the memory location to probe. Recent explicit expander constructions are shown to yield space usage much smaller than what would be required using a deterministic lookup procedure. Our data structure supports efficient deterministic updates, exhibiting new probabilistic guarantees on dictionary running time.
A Distributed Election and Spanning Tree Algorithm Based on Depth First Search
Authors: Skyum Sven
Published: February 2016

The existence of an effective traversal algorithm for a class of graphs has proven useful in connection with election problems for those classes. In this paper we show how a general traversal algorithm, such as depth first search, can be turned into an effective election algorithm using modular techniques. The presented method also constructs a spanning tree for the graph.
A Virtual Class Calculus
Authors: Ernst Erik , Ostermann Klaus , Cook William
Published: February 2016

Virtual classes are class-valued attributes of objects.
Like virtual methods, virtual classes are defined in
an object’s class and may be redefined within subclasses.
They resemble inner classes, which are also
defined within a class, but virtual classes are accessed
through object instances, not as static components
of a class. When used as types, virtual classes depend
upon object identity – each object instance introduces
a new family of virtual class types. Virtual classes support large-scale program composition techniques,
including higher-order hierarchies and family
polymorphism. The original definition of virtual
classes in Beta left open the question of static type
safety, since some type errors were not caught until
runtime. Later the languages Caesar and gbeta have
used a more strict static analysis in order to ensure
static type safety. However, the existence of a sound,
statically typed model for virtual classes has been a
long-standing open question. This technical report
presents a virtual class calculus, vc, that captures
the essence of virtual classes in these full-fledged programming languages. The key contributions of the
paper are a formalization of the dynamic and static
semantics of vc and a proof of the soundness of vc.
Categories: D.3.3 [Language Constructs and Features]:
Classes and objects, inheritance, polymorphism.
F.3.3 [Studies of Program Constructs]:
Object-oriented constructs, type structure. F.3.2
[Semantics of Programming Languages]: Operational
semantics.
Erotic Aspects of Everyday Life as a Challenge for Ubiquitous Computing
Authors: Bertelsen Olav , Petersen Marianne Graves
Published: February 2016

In this paper we discuss how interactive technology

disables or enables erotic aspects of everyday life, and we

discuss a number of design concepts in order to relate erotic

aspects to the issue of visibility versus invisibility in

ambient computing. This discussion has general relevance

for the study of residual categories in ubiquitous

computing.
Vehicular Mobility Prediction by Bayesian Networks
Authors: Schougaard Kari
Published: February 2016

In mobile and ubiquitous computing the location of devices
is often important both for the behavior of the applications
and for communication and other middleware functionality.
Mobility prediction enables proactively dealing
with changes in location dependent functionality. In this
project Bayesian networks’ ability to reason on the basis of
incomplete or inaccurate information is powering mobility
prediction based on a map of the street grid and the current
location and direction of the vehicle. We found that it
is feasible to divide information of a map into smaller parts
and generate a Bayesian network for each of these in order
to make mobility prediction based on localized information.
This makes the information stored in the Bayesian networks
more manageable in size, which is important for resource
constrained devices. Common sense knowledge of how vehicle
moves is feeded into the networks and enables them
to make a good prediction even when no information of the
vehicles mobility history is used. Experiments on real world
data show that in an area statically divided into hexagonal
cells of 200m in diameter, we get 80.54% accuracy when
using localized Bayesian networks to predict which cell a
vehicle enters next.
Optimal Resilient Dynamic Dictionaries⋆
Authors: Brodal Gerth Stølting , Fagerberg Rolf , Jørgensen Allan Grønlund , Moruz Gabriel , Mølhave Thomas
Published: February 2016

Abstract. In the resilient memory model any memory cell can get cor- rupted at any time, and corrupted cells cannot be distinguished from uncorrupted cells. An upper bound, , on the number of corruptions and O(1) reliable memory cells are provided. In this model, a data structure is denoted resilient if it gives the correct output on the set of uncor- rupted elements. We propose two optimal resilient static dictionaries, a randomized one and a deterministic one. The randomized dictionary supports searches in O(log n + ) expected time using O(log ) random bits in the worst case, under the assumption that corruptions are not performed by an adaptive adversary. The deterministic static dictionary supports searches in O(log n + ) time in the worst case. We also in- troduce a deterministic dynamic resilient dictionary supporting searches in O(log n + ) time in the worst case, which is optimal, and updates in O(log n + ) amortized time. Our dynamic dictionary supports range queries in O(log n + + k) worst case time, where k is the size of the output.
Process grammar and process history for 2D objects
Authors: Larsen Thomas W. , Mayoh Brian H.
Published: February 2016

This project is the written report for the course in Picture Processing at the Department of Computer Science, Aarhus University. The starting point is a paper by Michael Leyton in Artificial Intelligence 34, 1988: "A process grammar for shape". The paper describes how it is possible to derive the process history for an object from its state at two stages in its development. The aim of this project is to describe and test an algorithm for doing so.
Wii i Trige Et projekt om Wii, motivation og ældres træning.
Authors: Aarhus Rikke , Cedergren Anni , Grönvall Erik , Hald Anja Elgaard , Larsen Simon Bo , Moesgaard Tine , Wollsen Susanne
Published: February 2016

Projektet Wii i Trige (feb.-juli 2009) blev igangsat i forbindelse med Konsortiet for Brugerdreven Sundhedsinnovations arbejde med ældre og teknologi. Undersøgelsen har haft fokus på ældres anvendelse af Nintendo Wii, samt på hvorvidt computerspil  med fysisk interaktion kan motivere og bidrage til vedligeholdelsestræning og genoptræning på et lokalcenter. Projektet er gennemført af ansatte fra Lokalcenter Bjørnshøj, Datalogisk Institut og Alexandra Instituttet.
ECSCW 2011 Conference Supplement: European Conference on Computer-Supported Cooperative Work Aarhus, 24.-28. September 2011
Authors: Bødker Susanne
Published: February 2016

Dual eye-tracking (DUET) is a promising methodology to study and support

collaborative work. The method consists of simultaneously recording the gaze of two

collaborators working on a common task. The main themes addressed in the workshop

are eye-tracking methodology (how to translate gaze measures into descriptions of joint

action, how to measure and model gaze alignment between collaborators, how to address

task specificity inherent to eye-tracking data) and more generally future applications of

dual eye-tracking in CSCW. The DUET workshop will bring together scholars who

currently develop the approach as well as a larger audience interested in applications of

eye-tracking in collaborative situations. The workshop format will combine paper

presentations and discussions. The papers are available online as PDF documents at

http://www.dualeyetracking.org/DUET2011/.
Proceedings of Designing Self-care for Everyday Life. Workshop in conjunction with NordiCHI 2014, 27th October.
Authors: Verdezoto Nervo , Nunes Francisco , Grönvall Erik , Fitzpatrick Geraldine , Storni Cristiano , Kyng Morten
Published: February 2016

Managing chronic conditions can be challenging. People in such conditions, and the people around them, have to, for example: deal with symptoms, adapt to the resulting disability, manage emotions, and change habits to keep the condition under control. Self-care technologies have the potential to support self-care, however they often disregard the complexity of the settings in which they are used and fail to become integrated in everyday life.

The present collection of papers forms the Proceedings of the Workshop “Designing Selfcare for Everyday Life” conducted last October 27th, 2014 in Helsinki, where 14 participants from 7 different countries spent the day discussing how to design self-care technologies that are in harmony with people’s everyday life. During the morning, discussions were driven by poster presentations focused on the participants’ work. In the afternoon, we engaged in a
participatory design exercise focused on the self-care of Parkinson’s disease. Our discussions were driven by the experience of two people living with Parkinson’s that participated in our workshop. At the end of the exercise, each group presented the different insights, concepts and problems that each patient experiences in their everyday life with the disease. Last, we all engaged in a broader discussion with a mapping exercise of issues and challenges in relation to self-care.

The contributions featured in the proceedings have been peer-reviewed by the members of the Workshop Program Committee and selected on the basis of their quality, alignment with the workshop theme, and the extent (and diversity) of their backgrounds in design. They express points of view of researchers from both Academia and Industry and provide relevant insights in the design and development use of technologies for self-care.

We want to thank all the participants and co-authors for contributing to the Workshop. We are particularly grateful to the two patients, members of the Finnish Parkinson’s Association, who accepted to participate in the workshop and enabled researchers to get a
perspective on the challenges of their lives. We also want to thank all the Programme Committee members for all their work during the reviewing process as well as the organisers of NordiCHI 2014 for providing useful facilities.
Kollektivhuse – Hovedstaden på forkant
Authors: Bro Henning
Published: February 2016

Selv om der blev etableret visse fælles foranstaltninger i noget af det filantropiske byggeri, der skød frem i 1850'erne og 60'erne, hørte det egentlige kollektivhus det 20. århundrede til: En boligbebyggelse med selvstændige lejligheder, i nogle tilfælde for grupper med særlige boligbehov, med tilknyttede fællesfaciliteter for beboerne. I udgangspunktet centralkøkken med spisesal og restaurant, andre aflastende servicetilbud for den daglige husførelse, daginstitution, indkøbsmuligheder og senere tillige selskabslokaler, gæstehotel, hobbylokaler m.m.

Abstract
As one of the first places in Europe, cooperative housing was built on Frederiksberg in 1903 by a philanthropic building society under the management of principal Otte Fick. During the years 1916-1930, the Danish Welfare State's housing policy was established. In this connection, the municipality of Copenhagen stood behind the policy by subsidizing eight blocks of cooperative housing - in all
1,125 flats - through a considerable amount of public funds. In Copenhagen itself and on Frederiksberg, non-profit housing associations as well as entrepreneurs supported this policy.
While most of the cooperative housing had central kitchens with dining rooms, some had a number of common facilities such as day-care centres, domestic help and/or modern washers and dryers. Some of the cooperative housing also had a local grocery store for the residents and the surrounding neighbourhood.
The cooperative housing was planned by some of the leading architects of that era and the majority of the flats had a room with a box bed, a small kitchen and an entrance hall; and all the flats had a toilet, a shower, and central heating. There was also a plan which encompassed flats facing out to corridors. The design of the cooperative housing included closed or open courtyards, L-shaped houses,
or blocks of flats surrounded by small gardens. Furthermore, it was considered innovative to build residential properties intended for certain social groups that had specific housing requirements. On the housing market, it was particularly troublesome to acquire self-contained flats for single parents with children and
elderly women - primarily people from the working class and the lower middle class.
In 1930, the Danish capital, comprised of Copenhagen and Frederiksberg, was on the forefront of housing development compared to the rest of Denmark and internationally. It would also create an important foundation for widespread building construction of cooperative housing in the future. However, this type of housing never really caught on in the ordinary construction business in the
20th century. On the other hand, it succeeded in positioning itself as an essential means of housing especially for both handicapped and elderly people.
Indledning: Fortælling og fællesskab
Authors: Pedersen Marianne Holm , Andersen Lene
Published: February 2016

Alle mennesker fortæller historier. Hele dagen igennem fortæller vi og lytter tilhinandens historier - fra de små fortællinger over kaffen til de store fortællinger om nationens tilblivelse. Gennem andres fortællinger spejler tilhørerne sig selv og hører om det liv, der venter dem eller andre. De bliver vidne til, hvad der er godt og ondt, vigtigt eller ligegyldigt, og de ser langsomt verden folde sig ud i fælles øjenhøjde. Fortællinger er således tæt knyttet til skabelsen af fællesskaber. Dette nummer af Kulturstudier sætter fokus på sammenhængen mellem fortælling ogfællesskab og vil belyse, hvordan de historier, vi fortæller til os selv og om os selv, er med til at fylde de fællesskaber, som vi alle er en del af. Ved at bruge fortællingen som indgang til studiet af fællesskab kan man få indblik i, hvordan fællesskaber konstitueres, og hvad de konstitueres omkring - fx normer og værdier, rigtigt og forkert, lighed og forskellighed. De fem artikler i dette temanummer lægger vægten forskelligt - nogle fokuserer mere på fortællingen, andre mere påfællesskabet - men de giver fem eksempler på, hvordan fortælling og fællesskab kan forstås i forhold til hinanden.
Store og små fortællinger: Ritual og fællesskab blandt irakiske kvinder i København
Authors: Pedersen Marianne Holm
Published: February 2016

Inden for den antropologiske migrationsforskning har studier af fællesskab primært beskæftiget sig med fællesskaber relateret til migranternes nationale, religiøse eller politiske identiteter. Det er dog vigtigt også at inddrage de konkrete, sociale relationer, der opstår mellem migranterne det sted, hvor de bor. Denne artikel diskuterer, hvordan shia-muslimske irakiske kvinder i København igennemderes religiøse aktiviteter skaber forskellige former for fællesskab. Med udgangspunkt i en analyse af kalenderritualet muharram undersøger den, hvordan kvinderne i selve ritualet relaterer sig til religiøse og nationale fællesskaber, og hvorledes kvindernes øvrige sociale samvær kan lede til mere konkrete fællesskaber, der dog også har deres begrænsninger.

Great and Small Stories: Ritual and Community among Iraqi Women in Copenhagen

Anthropological research on migration has primarily studied the topic of community in relation to migrants' national, religious, or political identities. Yet, it is important to also explore the concrete, social relations that develop among imigrants at the place where they are currently living. This article investigates how Shia Muslim Iraqi women in Copenhagen use religious rituals and stories to construct different kinds of community. Based on an analysis of the calendrical rite of Muharram, it examines the ways in which the women through the ritualrelate to abstract communities drawing on their religious and national identities. It also explores how women's other social interactions may lead to more concretecommunities that are based on shared presence, activities, and the exchange of gossip and personal stories. The religious milieu gains its importance because women can negotiate their sense of belonging in relation to both their socio-culturalbackground and their everyday lives as part of an ethnic minority in Denmark. Nevertheless, the sense of community constructed among women does not necessarily extend outside of the religious activities. The article argues that it is necessary to thoroughly examine the sometimes contingent forms of community and belonging constructed among ethnic minorities rather than taking for granted that such communities exist on the basis of people's shared point of origin.
Med troen som fællesnævner – fællesskab blandt unge i Indre Mission
Authors: Christensen Tina Wilchen
Published: February 2016

Artiklen vil belyse de mekanismer, der ligger til grund for et velfungerende fællesskab i en af Indre Missions ungdomsforeninger i Århus. Troen har på forskellige måder en central position i fællesskabet, og denne artikel vil argumentere for de unges tro som en social identitet, idet deres habitus synes at have en afgørende betydning for den og deres oplevelse af det religiøst funderede fællesskab. Artiklenvil også belyse, hvordan Biblen og dens fortællinger udgør den fortolkningsramme, som de unge er opvokset med og forstår livet igennem. Artiklen viser desuden den rolle, det kollektive samvær spiller i de unges konstruktion af Gud og egen identitet som kristen.

Faith as common ground- community feeling among young evangelicals in Denmark

The aim of this article is to demonstrate the mechanisms that underlie a youth association in the so-called Home Mission, a branch of the Evangelical Lutheran Church of Denmark. It is the result of anthropological research focusing on the sense of community among members aged between 15 and 27. In a number of ways faith plays a central role in the community, and the main argument of the article is that the young people's faith constitutes a social identity, since their habitus seems to have a decisive impact on their experience of the faith-based community. The article further demonstrates how the Bible and its narratives form the framework of interpretation with which the young people have grown up, and which, in their present life as adults, continues to mould their understanding and view of life, as well as the role that collective interaction plays in the young people's construction of God and their own identity as Christians. A core argument in the article is that faith is a socialization into a structure which results in all participants having the same frame of reference and therefore experiencing a strong feeling of community with one another within this particular wing of the Church of Denmark. 