bluuebunny/crossref_metadata_2025 huggingface dataset:
Growing Languages with Metamorphic Syntax Macros
Authors: Brabrand Claus , Schwartzbach Michael I.
Published: February 2016

"From now on, a main goal in designing a language should be to plan for growth."
Guy Steele: Growing a Language, OOPSLA'98 invited talk.
We present our experiences with a syntax macro language augmented with a concept of metamorphisms. We claim this forms a general abstraction mechanism for
growing (domain-specific) extensions of programming languages.
Our syntax macros are similar to previous work in that the compiler accepts collections of grammatical rules that extend the syntax in which a subsequent program may be written. We exhibit how almost arbitrary extensions can be defined in a purely declarative manner without resorting to compile-time programming. The macros are
thus terminating in that parsing is guaranteed to terminate, hygienic since full-conversion eliminates the risk of name clashes, and transparent such that subsequent phases in the compiler are unaware of them. Error messages from later phases in the compiler are tracked through all macro invocations to pinpoint their sources in the extended syntax. A concept of metamorphic rules allows the arguments of a macro to be defined
in an almost arbitrary meta level grammar and then to be morphed into the host language. We show through examples how creative use of metamorphic syntax macros may be used not only to create convenient shorthand notation but also to introduce new
language concepts and mechanisms. In fact, whole new languages can be created at surprisingly low cost. The resulting programs are significantly easier to understand and maintain.
This work is fully implemented as part of the  system for defining
interactive Web services, but could find use in many other languages.
Inductive * -Semirings
Authors: Ésik Zoltán , Kuich Werner
Published: February 2016

One of the most well-known induction principles in computer science
is the fixed point induction rule, or least pre-fixed point rule. Inductive
*-semirings are partially ordered semirings equipped with a star operation
satisfying the fixed point equation and the fixed point induction rule for
linear terms. Inductive *-semirings are extensions of continuous semirings
and the Kleene algebras of Conway and Kozen.
We develop, in a systematic way, the rudiments of the theory of inductive
*-semirings in relation to automata, languages and power series.
In particular, we prove that if S is an inductive *-semiring, then so is
the semiring of matrices Sn*n, for any integer n >= 0, and that if S is
an inductive *-semiring, then so is any semiring of power series S((A*)).
As shown by Kozen, the dual of an inductive *-semiring may not be inductive.
In contrast, we show that the dual of an iteration semiring is
an iteration semiring. Kuich proved a general Kleene theorem for continuous
 semirings, and Bloom and Esik proved a Kleene theorem for all Conway
semirings. Since any inductive *-semiring is a Conway semiring
and an iteration semiring, as we show, there results a Kleene theorem
applicable to all inductive *-semirings. We also describe the structure
of the initial inductive *-semiring and conjecture that any free inductive
*-semiring may be given as a semiring of rational power series with
coefficients in the initial inductive *-semiring. We relate this conjecture to
recent axiomatization results on the equational theory of the regular sets.
Free mu-lattices
Authors: Santocanale Luigi
Published: February 2016

A mu-lattice is a lattice with the property that every unary
polynomial has both a least and a greatest fix-point. In this paper
we define the quasivariety of mu-lattices and, for a given partially
ordered set P, we construct a mu-lattice JP whose elements are
equivalence classes of games in a preordered class J (P). We prove
that the mu-lattice JP is free over the ordered set P and that the
order relation of JP is decidable if the order relation of P is
decidable. By means of this characterization of free mu-lattices we
infer that the class of complete lattices generates the quasivariety
of mu-lattices.
Keywords: mu-lattices, free mu-lattices, free lattices, bicompletion
of categories, models of computation, least and greatest fix-points,
mu-calculus, Rabin chain games.
On Memory-Block Traversal Problems in Model Checking Timed Systems
Authors: Larsson Fredrik , Pettersson Paul , Yi Wang
Published: February 2016

A major problem in model-checking timed systems is the
huge memory requirement. In this paper, we study the memory-block
traversal problems of using standard operating systems in exploring the
state-space of timed automata. We report a case study which demonstrates
that deallocating memory blocks (i.e. memory-block traversal)
using standard memory management routines is extremely time-consuming.
The phenomenon is demonstrated in a number of experiments by
installing the Uppaal tool on Windows95, SunOS 5 and Linux. It seems
that the problem should be solved by implementing a memory manager
for the model-checker, which is a troublesome task as it is involved in
the underlining hardware and operating system. We present an alternative
technique that allows the model-checker to control the memory-block
traversal strategies of the operating systems without implementing
an independent memory manager. The technique is implemented in the
Uppaal model-checker. Our experiments demonstrate that it results in
significant improvement on the performance of Uppaal. For example, it
reduces the memory deallocation time in checking a start-up synchronisation
protocol on Linux from 7 days to about 1 hour. We show that the
technique can also be applied in speeding up re-traversals of explored
state-space.
Partial Evaluation of Pattern Matching in Strings, revisited
Authors: Grobauer Bernd , Lawall Julia L.
Published: February 2016

Specializing string matchers is a canonical example of partial evaluation.
 A naive implementation of a string matcher repeatedly matches a
pattern against every substring of the data string; this operation should
intuitively benefit from specializing the matcher with respect to the pattern.
 In practice, however, producing an efficient implementation by
performing this specialization using standard partial-evaluation techniques
has been found to require non-trivial binding-time improvements. Starting
 with a naive matcher, we thus present a derivation of a binding-time
improved string matcher. We prove its correctness and show that specialization
 with respect to a pattern yields a matcher with code size linear
in the length of the pattern and running time linear in the length of its
input. We then consider several variants of matchers that specialize well,
amongst them the first such matcher presented in the literature, and we
demonstrate how variants can be derived from each other systematically.
The Meaning of Types From Intrinsic to Extrinsic Semantics
Authors: Reynolds John C.
Published: February 2016

A definition of a typed language is said to be "intrinsic" if it assigns
meanings to typings rather than arbitrary phrases, so that ill-typed
phrases are meaningless. In contrast, a definition is said to be "extrinsic"
if all phrases have meanings that are independent of their typings,
while typings represent properties of these meanings.
For a simply typed lambda calculus, extended with recursion, subtypes,
and named products, we give an intrinsic denotational semantics
and a denotational semantics of the underlying untyped language. We
then establish a logical relations theorem between these two semantics,
and show that the logical relations can be "bracketed" by retractions
between the domains of the two semantics. From these results, we
derive an extrinsic semantics that uses partial equivalence relations.
A Simple Take on Typed Abstract Syntax in Haskell-like Languages
Authors: Danvy Olivier , Rhiger Morten
Published: February 2016

We present a simple way to program typed abstract syntax in a
language following a Hindley-Milner typing discipline, such as Haskell and ML, and we apply it to automate two proofs about normalization functions as embodied in type-directed partial evaluation for the simply typed lambda calculus: normalization functions (1) preserve types and (2) yield long beta-eta normal forms.

Keywords: Type-directed partial evaluation, normalization functions, simply-typed lambda-calculus, higher-order abstract syntax, Haskell.
CPS Transformation of Beta-Redexes
Authors: Danvy Olivier , Nielsen Lasse R.
Published: February 2016

The extra compaction of Sabry and Felleisen's transformation is due to making continuations occur first in CPS terms and classifying more redexes as administrative. We show that the extra compaction is actually independent of the relative positions of values and continuations and furthermore that it is solely due to a context-sensitive transformation of beta-redexes. We stage the more compact CPS transformation into a first-order uncurrying phase and a context-insensitive CPS transformation. We also dene a context-insensitive CPS transformation that is just as compact. This CPS transformation operates in one pass and is dependently typed.

Keywords: Continuation-passing style (CPS), Plotkin, Fischer, one-pass CPS
transformation, two-level lambda-calculus, generalized reduction.
The Pointer Assertion Logic Engine
Authors: Møller Anders , Schwartzbach Michael I.
Published: February 2016

We present a new framework for verifying partial specifications of programs in order to catch type and memory errors and check data structure invariants. Our technique can verify a large class of data structures, namely all those that can be expressed as graph types. Earlier versions were restricted to simple
special cases such as lists or trees. Even so, our current implementation is as fast as the previous specialized tools.
Programs are annotated with partial specifications expressed in Pointer Assertion Logic, a new notation for expressing properties of the program store. We work in the logical tradition by encoding the programs and partial specifications as formulas in monadic second-order logic. Validity of these formulas
is checked by the MONA tool, which also can provide explicit counterexamples to invalid formulas.
Other work with similar goals is based on more traditional program analyses, such as shape analysis. That approach requires explicit introduction of an appropriate operational semantics along with a proof of correctness whenever
a new data structure is being considered. In comparison, our approach only requires the data structure to be abstractly described in Pointer Assertion Logic.
MONA Implementation Secrets
Authors: Klarlund Nils , Møller Anders , Schwartzbach Michael I.
Published: February 2016

The MONA tool provides an implementation of automaton-based decision procedures for the logics WS1S and WS2S. It has been used for numerous applications, and it is remarkably efficient in practice, even though it faces a theoretically non-elementary worst-case complexity. The implementation has matured over a period of six years. Compared to the
first naive version, the present tool is faster by several orders of magnitude. This speedup is obtained from many different contributions working on all levels of the compilation and execution of formulas. We present
an overview of MONA and a selection of implementation "secrets" that have been discovered and tested over the years, including formula reductions, DAGification, guided tree automata, three-valued logic, eager minimization, BDD-based automata representations, and cache-conscious data structures. We describe these techniques and quantify their respective effects by experimenting with separate versions of the MONA tool that in turn omit each of them.
A Denotational Investigation of Defunctionalization
Authors: Nielsen Lasse R.
Published: February 2016

Defunctionalization was introduced by John Reynolds in his 1972
article Definitional Interpreters for Higher-Order Programming
Languages. Defunctionalization transforms a higher-order program into a first-order one, representing functional values as data structures. Since then it has been used quite widely, but we observe that it has never been proven correct. We formalize defunctionalization denotationally for a typed functional language, and we prove that it preserves the meaning of any terminating program. Our proof uses logical relations.

Keywords: defunctionalization, program transformation, denotational semantics, logical relations.
Improved Non-Committing Encryption Schemes based on a General Complexity Assumption
Authors: Damgård Ivan B. , Nielsen Jesper Buus
Published: February 2016

Non-committing encryption enables the construction of multiparty computation protocols secure against an adaptive adversary in the computational setting where private channels between players are not assumed. While any non-committing encryption scheme must be secure in the ordinary semantic sense, the converse is not necessarily true. We propose a construction of non-committing encryption that can be based on any public key system which is secure in the ordinary sense and which has an extra property we call simulatability. The construction contains an earlier proposed scheme by Beaver based on the Die-Hellman problem as a special case, and we propose another implementation based on RSA. In a more general setting, our construction can be based on any collection of trapdoor one-way permutations
with a certain simulatability property. This offers a considerable efficiency
improvement over the first non-committing encryption scheme proposed by
Canetti et al. Finally, at some loss of efficiency, our scheme can be based on general collections of trapdoor one-way permutations without the simulatability assumption, and without the common domain assumption of Canetti et al.
Democratic Consensus and the Local Majority Rule
Authors: Mustafa Nabil H. , Pekec Aleksandar
Published: February 2016

In this paper we study a rather generic communication/
coordination/ computation problem: in a finite network of agents,
each initially having one of the two possible states, can the majority
 initial state be computed and agreed upon (i.e., can a democratic
 consensus be reached) by means of iterative application of
the local majority rule. We show that this task is failure-free only
in the networks that are nowhere truly local. In other words, the
idea of solving a truly global task (reaching consensus on majority
) by means of truly local computation only (local majority rule)
is doomed for failure.
We also show that even well connected networks of agents that
are nowhere truly local might fail to reach democratic consensus
when the local majority rule is applied iteratively. Structural
properties of democratic consensus computers, i.e., the networks
in which iterative application of the local majority rule always
yields consensus in the initial majority state, are presented.
The Complexity of Constructing Evolutionary Trees Using Experiments
Authors: Brodal Gerth Stølting , Fagerberg Rolf , Pedersen Christian N. S. , Östlin Anna
Published: February 2016

We present tight upper and lower bounds for the problem of constructing evolutionary trees in the experiment model. We describe an algorithm which constructs an evolutionary tree of n species in time O(n d logd n) using at most n |d/2| (log2|d/2|−1 n + O(1)) experiments for d > 2, and
at most n(log n + O(1)) experiments for d = 2, where d is the degree of the tree. This improves the previous best upper bound by a factor Theta(log d). For d = 2 the previously best algorithm with running time O(n log n) had a bound of 4n log n on the number of experiments. By an explicit adversary argument, we show an
Omega(nd logd n) lower bound, matching our upper bounds and improving the previous best lower bound
by a factor Theta(logd n). Central to our algorithm is the construction and maintenance of separator trees of small height. We present how to maintain separator trees with height log n + O(1) under the insertion of new nodes in amortized time O(log n). Part of our dynamic algorithm is an algorithm for computing a centroid tree in optimal time O(n).

Keywords: Evolutionary trees, Experiment model, Separator trees, Centroid tree, Lower bounds
Do we Need Dependent Types?
Authors: Fridlender Daniel , Indrika Mia
Published: February 2016

Inspired by [1], we describe a technique for defining, within the
Hindley-Milner type system, some functions which seem to require a
language with dependent types. We illustrate this by giving a general
definition of zipWith for which the Haskell library provides a family
of functions, each member of the family having a different type and
arity. Our technique consists in introducing ad hoc codings for natural
numbers which resemble numerals in lambda-calculus.
Language-Based Caching of Dynamically Generated HTML
Authors: Brabrand Claus , Møller Anders , Olesen Steffan , Schwartzbach Michael I.
Published: February 2016

Increasingly, HTML documents are dynamically generated by interactive Web
services. To ensure that the client is presented with the newest versions of such
documents it is customary to disable client caching causing a seemingly inevitable performance penalty. In the  system, dynamic HTML documents are composed of higher-order templates that are plugged together to construct complete documents. We show how to exploit this feature to provide an automatic fine-grained caching of document templates, based on the service source code. A  service transmits not the full HTML document but instead a compact JavaScript recipe for a client-side construction of the document based on a static collection of fragments that can be cached by the browser in the usual manner. We compare our approach with related techniques and demonstrate on a number of realistic benchmarks that the size of the transmitted data and the latency may be reduced significantly.
On the Power of Labels in Transition Systems
Authors: Srba Jirí
Published: February 2016

In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of mu-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets.
Optimal Time-Space Trade-Offs for Non-Comparison-Based Sorting
Authors: Pagh Rasmus , Pagter Jakob
Published: February 2016

We study the fundamental problem of sorting n integers of w bits on a unit-cost RAM with word size w, and in particular consider the time-space trade-off (product of time and space in bits) for this problem. For comparison-based algorithms, the time-space complexity is known to be Theta(n^2). A result of Beame shows that the lower bound also holds for non-comparison-based algorithms, but no algorithm has met this for time below the comparison-based
Omega(n lg n) lower bound. 

We show that if sorting within some time bound T~ is possible, then time T = O(T~ + n lg* n) can be achieved with high probability using space S = O(n^2/T + w), which is optimal. Given a deterministic priority queue using amortized
time t(n) per operation and space n^O(1), we provide a deterministic
algorithm sorting in time T = O(n (t(n) + lg* n)) with S = O(n^2/T+w). Both results require that w <= n^(1-Omega(1)).

Using existing priority queues and sorting algorithms, this implies
that we can deterministically sort time-space optimally in time Theta(T) for T >= n(lg lg n)^2, and with high probability for T >= n lg lg n.

Our results imply that recent lower bounds for deciding element distinctness in o(n lg n) time are nearly tight.
A Complete Axiomatization of Simulation for Regular CCS Expressions
Authors: Frendrup Ulrik , Jensen Jesper Nyholm
Published: February 2016

This paper gives axiomatizations of strong and weak simulation over regular CCS expressions. The proof of completeness of the axiomatization of strong simulation is inspired by Milner's proof of completeness of his axiomatization for strong equivalence over regular CCS expressions. Soundness and completeness of the axiomatization for weak simulation is easily deduced from the corresponding result for the axiomatization of strong simulation over regular CCS expressions.
A Higher-Order Calculus for Categories
Authors: Cáccamo Mario Jose , Winskel Glynn
Published: February 2016

A calculus for a fragment of category theory is presented. The types in the language denote categories and the expressions functors. The judgements of the calculus systematise categorical arguments such as: an expression is functorial in its free variables; two expressions are naturally isomorphic in their free variables. There are special binders for limits and more general ends. The rules for limits and ends support an algebraic manipulation of universal constructions as opposed to a more traditional diagrammatic approach. Duality within the calculus and applications in proving continuity are discussed with examples. The calculus gives a basis for mechanising a theory of categories in a generic theorem prover like Isabelle.
Lossy Dictionaries
Authors: Pagh Rasmus , Rodler Flemming Friche
Published: February 2016

Bloom filtering is an important technique for space efficient storage of a conservative approximation of a set S. The set stored may have up to some specified number of "false positive'' members, but all elements of S are included. In this paper we consider lossy dictionaries that are also allowed to have "false negatives'', i.e., leave out elements of S. The aim is to maximize the weight of included keys within a given space constraint. This relaxation allows a very fast and simple data structure making almost optimal use of memory. Being more time efficient than Bloom filters, we believe our data structure to be well suited for replacing Bloom filters in some applications. Also, the fact that our data structure supports information associated to keys paves the way for new uses, as illustrated by an application in lossy image compression.
Fast Random Access to Wavelet Compressed Volumetric Data Using Hashing
Authors: Rodler Flemming Friche , Pagh Rasmus
Published: February 2016

We present a new approach to lossy storage of the coefficients of wavelet transformed data. While it is common to store the coefficients of largest magnitude (and let all other coefficients be zero), we allow a slightly different set of coefficients to be stored. This brings into play a recently proposed hashing technique that allows space efficient storage and very efficient retrieval of coefficients. Our approach is applied to compression of volumetric data sets. For the ``Visible Man'' volume we obtain up to 80% improvement in compression ratio over previously suggested schemes. Further, the time for accessing a random voxel is quite competitive.
CPS Transformation of Flow Information, Part II: Administrative Reductions
Authors: Damian Daniel , Danvy Olivier
Published: February 2016

We characterize the impact of a linear beta-reduction on the result of a control-flow analysis. (By ``a linear beta-reduction'' we mean the beta-reduction of a linear lambda-abstraction, i.e., of a lambda-abstraction whose parameter occurs exactly once in its body.)

 As a corollary, we consider the administrative reductions of a Plotkin-style transformation into continuation-passing style (CPS), and how they affect the result of a constraint-based control-flow analysis and in particular the least element in the space of solutions. We show that administrative reductions preserve the least solution. Since we know how to construct least solutions, preservation of least solutions solves a problem that was left open in Palsberg and Wand's paper ``CPS Transformation of Flow Information.''

Therefore, together, Palsberg and Wand's article ``CPS Transformation of Flow Information'' and the present article show how to map, in linear time, the least solution of the flow constraints of a program into the least solution of the flow constraints of the CPS counterpart of this program, after administrative reductions. Furthermore, we show how to CPS transform control-flow information in one pass.

Superseded by BRICS-RS-02-36.
Non-Committing Encryption is Too Easy in the Random Oracle Model
Authors: Nielsen Jesper Buus
Published: February 2016

The non-committing encryption problem arises in the setting of adaptively secure cryptographic protocols, as the task of implementing secure channels. We prove that in the random oracle model, where the parties have oracle access to a uniformly random function, non-committing encryption can be implemented efficiently using any trapdoor permutation.

We also prove that no matter how the oracle is instantiated in practice the resulting scheme will never be non-committing, and we give a short discussion of the random oracle model in light of this.
On the Number of Quasi-Kernels in Digraphs
Authors: Gutin Gregory , Koh Khee Meng , Tay Eng Guan , Yeo Anders
Published: February 2016

A vertex set X of a digraph D = (V,A) is a kernel if X is independent
 (i.e., all pairs of distinct vertices of X are non-adjacent) and for
every v in V − X there exists x in X such that vx in A. A vertex set
X of a digraph D = (V,A) is a quasi-kernel if X is independent and
for every v in V − X there exist w in V − X, x in X such that either
vx in A or vw,wx in A: In 1994, Chvatal and Lovasz proved that every
digraph has a quasi-kernel. In 1996, Jacob and Meyniel proved that,
if  a digraph D has no kernel, then D contains at least three quasi-kernels.

We characterize digraphs with exactly one and two quasi-kernels, and,
thus, provide necessary and sufficient conditions for a digraph to have
at least three quasi-kernels. In particular, we prove that every strong
digraph of order at least three, which is not a 4-cycle, has at least
three quasi-kernels. We conjecture that every digraph with no sink
has a pair of disjoint quasi-kernels and provide some support to this
conjecture.
The bigwig Project
Authors: Brabrand Claus , Møller Anders , Schwartzbach Michael I.
Published: February 2016

We present the results of the  project, which aims to design and implement a high-level domain-specific language for programming interactive Web services.

A fundamental aspect of the development of the World Wide Web during the last decade is the gradual change from static to dynamic generation of Web pages. Generating Web pages dynamically in dialogue with the client has the advantage of providing up-to-date and tailor-made information. The development of systems for constructing such dynamic Web services has emerged as a whole new research area.

The  language is designed by analyzing its application domain and identifying fundamental aspects of Web services inspired by problems and solutions in existing Web service development languages. The core of the design consists of a session-centered service model together with a flexible template-based mechanism for dynamic Web page construction. Using specialized program analyses, certain Web specific properties are verified at compile-time, for instance that only valid HTML 4.01 is ever shown to the clients. In addition, the design provides high-level solutions to form field validation, caching of dynamic pages, and temporal-logic based concurrency control, and it proposes syntax macros for making highly domain-specific languages. The language is implemented via widely available Web technologies, such as Apache on the server-side and JavaScript and Java Applets on the client-side. We conclude with experience and evaluation of the project.
Solving the String Statistics Problem in Time O(n log n)
Authors: Brodal Gerth Stølting , Lyngsø Rune B. , Östlin Anna , Pedersen Christian N. S.
Published: February 2016

The string statistics problem consists of preprocessing a string of length  n such that given a query pattern of length  m, the maximum number of non-overlapping occurrences of the query pattern in the string can be reported efficiently. Apostolico and Preparata introduced the minimal augmented suffix tree (MAST) as a data structure for the string statistics problem, and showed how to construct the MAST in time O(n log^2 n) and how it supports queries in time  O(m) for constant sized alphabets. A subsequent theorem by Fraenkel and Simpson stating that a string has at most a linear number of distinct squares implies that the MAST requires space  O(n). In this paper we improve the construction time for the MAST to O(n log n) by extending the algorithm of Apostolico and Preparata to exploit properties of efficient joining and splitting of search trees together with a refined analysis.
Modified Bar Recursion
Authors: Berger Ulrich , Oliva Paulo B.
Published: February 2016

We introduce a variant of Spector's bar recursion (called "modified bar recursion'') in finite types to give a realizability interpretation of the classical axiom of countable choice allowing for the extraction of witnesses from proofs of Sigma_1 formulas in classical analysis. As a second application of modified bar recursion we present a bar recursive definition of the fan functional. Moreover, we show that modified bar recursion exists in M (the model of strongly majorizable functionals) and is not S1-S9 computable in C (the model of total functionals). Finally, we show that modified bar recursion defines Spector's bar recursion primitive recursively.
On the Number of Maximal Bipartite Subgraphs of a Graph
Authors: Madsen Bolette Ammitzbøll , Byskov Jesper Makholm , Skjernaa Bjarke
Published: February 2016

We show new lower and upper bounds on the number of maximal induced bipartite subgraphs of graphs with n vertices. We present an infinite family of graphs having 105^{n/10} ~= 1.5926^n such subgraphs, which improves an earlier lower bound by Schiermeyer (1996). We show an upper bound of n . 12^{n/4} ~= n . 1.8613^n and give an algorithm that lists all maximal induced bipartite subgraphs in time proportional to this bound. This is used in an algorithm for checking 4-colourability of a graph running within the same time bound.
Cache Oblivious Distribution Sweeping
Authors: Brodal Gerth Stølting , Fagerberg Rolf
Published: February 2016

We adapt the distribution sweeping method to the cache oblivious model. Distribution sweeping is the name used for a general approach for divide-and-conquer algorithms where the combination of solved subproblems can be viewed as a merging process of streams. We demonstrate by a series of algorithms for specific problems the feasibility of the method in a cache oblivious setting. The problems all come from computational geometry, and are: orthogonal line segment intersection reporting, the all nearest neighbors problem, the 3D maxima problem, computing the measure of a set of axis-parallel rectangles, computing the visibility of a set of line segments from a point, batched orthogonal range queries, and reporting pairwise intersections of axis-parallel rectangles. Our basic building block is a simplified version of the cache oblivious sorting algorithm Funnelsort of Frigo et al., which is of independent interest.

 

Full text: http://dx.doi.org/10.1007/3-540-45465-9_37
An Extension Theorem with an Application to Formal Tree Series
Authors: Bloom Stephen L. , Ésik Zoltán
Published: February 2016

A grove theory is a Lawvere algebraic theory T for which each hom-set T(n,p) is a commutative monoid; composition on the right distributes over all finite sums: (\sum f_i) . h = \sum f_i . h. A matrix theory is a grove theory in which composition on the left and right distributes over finite sums. A matrix theory M is isomorphic to a theory of all matrices over the semiring S = M(1,1). Examples of grove theories are theories of (bisimulation equivalence classes of) synchronization trees, and theories of formal tree series over a semiring S . Our main theorem states that if T is a grove theory which has a matrix subtheory M which is an iteration theory, then, under certain conditions, the fixed point operation on M can be extended in exactly one way to a fixed point operation on T such that T is an iteration theory. A second theorem is a Kleene-type result. Assume that T is an iteration grove theory and M is a sub iteration grove theory of T which is a matrix theory. For a given collection Sigma of scalar morphisms in T we describe the smallest sub iteration grove theory of T containing all the morphisms in M union Sigma .
Formal Tree Series
Authors: Ésik Zoltán , Kuich Werner
Published: February 2016

In this survey we generalize some results on formal tree languages, tree grammars and tree automata by an algebraic treatment using semirings, fixed point theory, formal tree series and matrices. The use of these mathematical constructs makes definitions, constructions, and proofs more satisfactory from an mathematical point of view than the customary ones. The contents of this survey paper is indicated by the titles of the sections:1.Introduction2.Preliminaries3.Tree automata and systems of equations4.Closure properties and a Kleene Theorem for recognizable tree series5.Pushdown tree automata, algebraic tree systems, and a Kleene Theorem6.Tree series transducers7.Full abstract families of tree series8.Connections to formal power series
Simulating Uniform Hashing in Constant Time and Optimal Space
Authors: Östlin Anna , Pagh Rasmus
Published: February 2016

Many algorithms and data structures employing hashing have been analyzed under the uniform hashing assumption, i.e., the assumption that hash functions behave like truly random functions. In this paper it is shown how to implement hash functions that can be evaluated on a RAM in constant time, and behave like truly random functions on any set of n inputs, with high probability. The space needed to represent a function is O(n) words, which is the best possible (and a polynomial improvement compared to previous fast hash functions). As a consequence, a broad class of hashing schemes can be implemented to meet, with high probability, the performance guarantees of their uniform hashing analysis.
Comparative Methods for Gene Structure Prediction in Homologous Sequences
Authors: Pedersen Christian N. S. , Scharling Tejs
Published: February 2016

The increasing number of sequenced genomes motivates the use of evolutionary patterns to detect genes. We present a series of comparative methods for gene finding in homologous prokaryotic or eukaryotic sequences. Based on a model of legal genes and a similarity measure between genes, we find the pair of legal genes of maximum similarity. We develop methods based on genes models and alignment based similarity measures of increasing complexity, which take into account many details of real gene structures, e.g. the similarity of the proteins encoded by the exons. When using a similarity measure based on an exiting alignment, the methods run in linear time. When integrating the alignment and prediction process which allows for more fine grained similarity measures, the methods run in quadratic time. We evaluate the methods in a series of experiments on synthetic and real sequence data, which show that all methods are competitive but that taking the similarity of the encoded proteins into account really boost the performance.
Memoization in Type-Directed Partial Evaluation
Authors: Balat Vincent , Danvy Olivier
Published: February 2016

We use a code generator--type-directed partial evaluation--to verify conversions between isomorphic types, or more precisely to verify that a composite function is the identity function at some complicated type. A typed functional language such as ML provides a natural support to express the functions and type-directed partial evaluation provides a convenient setting to obtain the normal form of their composition. However, off-the-shelf type-directed partial evaluation turns out to yield gigantic normal forms.

We identify that this gigantism is due to redundancies, and that these redundancies originate in the handling of sums, which uses delimited continuations. We successfully eliminate these redundancies by extending type-directed partial evaluation with memoization capabilities. The result only works for pure functional programs, but it provides an unexpected use of code generation and it yields orders-of-magnitude improvements both in time and in space for type isomorphisms.
Timed Automata May Cause Some Troubles
Authors: Bouyer Patricia
Published: February 2016

Timed automata are a widely studied model. Its decidability has been proved using the so-called region automaton construction. This construction provides a correct abstraction for the behaviours of timed automata, but it does not support a natural implementation and, in practice, algorithms based on the notion of zones are implemented using adapted data structures like DBMs. When we focus on forward analysis algorithms, the exact computation of all the successors of the initial configurations does not always terminate. Thus, some abstractions are often used to ensure termination, among which, a widening operator on zones.

In this paper, we study in details this widening operator and the forward analysis algorithm that uses it. This algorithm is most used and implemented in tools like Kronos and Uppaal. One of our main results is that it is hopeless to find a forward analysis algorithm, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in details this algorithm in the more general framework of updatable timed automata, a model which has been introduced as a natural syntactic extension of classical timed automata. We describe subclasses of this model for which a correct widening operator can be found.
Syntactic Theories in Practice
Authors: Danvy Olivier , Nielsen Lasse R.
Published: February 2016

The evaluation function of a syntactic theory is canonically defined as the transitive closure of (1) decomposing a program into an evaluation context and a redex, (2) contracting this redex, and (3) plugging the contractum in the context. Directly implementing this evaluation function therefore yields an interpreter with a worst-case overhead, for each step, that is linear in the size of the input program. We present sufficient conditions over a syntactic theory to circumvent this overhead, by replacing the composition of (3) plugging and (1) decomposing by a single ``refocusing'' function mapping a contractum and a context into a new context and a new redex, if there are any. We also show how to construct such a refocusing function, we prove its correctness, and we analyze its complexity.

We illustrate refocusing with two examples: a programming-language interpreter and a transformation into continuation-passing style. As a byproduct, the time complexity of this program transformation is mechanically changed from quadratic in the worst case to linear.
Checking Consistency of Pedigree Information is NP-complete (Preliminary Report)
Authors: Aceto Luca , Hansen Jens Alsted , Ingólfsdóttir Anna , Johnsen Jacob , Knudsen John
Published: February 2016

Consistency checking is a fundamental computational problem in genetics. Given a pedigree and information on the genotypes of some of the individuals in it, the aim of consistency checking is to determine whether these data are consistent with the classic Mendelian laws of inheritance. This problem arose originally from the geneticists' need to filter their input data from erroneous information, and is well motivated from both a biological and a sociological viewpoint. This paper shows that consistency checking is NP-complete, even in the presence of three alleles. Several other results on the computational complexity of problems from genetics that are related to consistency checking are also offered. In particular, it is shown that checking the consistency of pedigrees over two alleles can be done in polynomial time.
Higher Dimensional Automata
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.
Circuits on Cylinders
Authors: Hansen Kristoffer Arnsfelt , Miltersen Peter Bro , Vinay V.
Published: February 2016

We consider the computational power of constant width polynomial size cylindrical circuits and nondeterministic branching programs. We show that every function computed by a Pi_2 o MOD o AC^0 circuit can also be computed by a constant width polynomial size cylindrical nondeterministic branching program (or cylindrical circuit) and that every function computed by a constant width polynomial size cylindrical circuit belongs to ACC^0.
Computing Refined Buneman Trees in Cubic Time
Authors: Brodal Gerth Stølting , Fagerberg Rolf , Östlin Anna , Pedersen Christian N. S. , Rao S. Srinivasa
Published: February 2016

Reconstructing the evolutionary tree for a set of n  species based on pairwise distances between the species is a fundamental problem in bioinformatics. Neighbour joining is a popular distance based tree reconstruction method. It always proposes fully resolved binary trees despite missing evidence in the underlying distance data. Distance based methods based on the theory of Buneman trees and refined Buneman trees avoid this problem by only proposing evolutionary trees whose edges satisfy a number of constraints. These trees might not be fully resolved but there is strong combinatorial evidence for each proposed edge. The currently best algorithm for computing the refined Buneman tree from a given distance measure has a running time of O(n^5) and a space consumption of O(n^4). In this paper, we present an algorithm with running time  O(n^3) and space consumption  O(n^2).
A Formalization of Linkage Analysis
Authors: Ingólfsdóttir Anna , Christensen Anders Lyhne , Hansen Jens Alsted , Johnsen Jacob , Knudsen John , Rasmussen Jacob Illum
Published: February 2016

In this report a formalization of genetic linkage analysis is introduced. Linkage analysis is a computationally hard biomathematical method, which purpose is to locate genes on the human genome. It is rooted in the new area of bioinformatics and no formalization of the method has previously been established. Initially, the biological model is presented. On the basis of this biological model we establish a formalization that enables reasoning about algorithms used in linkage analysis. The formalization applies both for single and multi point linkage analysis. We illustrate the usage of the formalization in correctness proofs of central algorithms and optimisations for linkage analysis. A further use of the formalization is to reason about alternative methods for linkage analysis. We discuss the use of MTBDDs and PDGs in linkage analysis, since they have proven efficient for other computationally hard problems involving large state spaces. We conclude that none of the techniques discussed are directly applicable to linkage analysis, however further research is needed in order to investigated whether a modified version of one or more of these are applicable.
GPU Accelerated Viscous-fluid Deformable Registration for Radiotherapy
Authors: Noe Karsten Østergaard , Tanderup Kari , Lindegaard Jacob Christian , Grau Cai , Sørensen Thomas Sangild
Published: February 2016

In cancer treatment organ and tissue deformation between
radiotherapy sessions represent a significant challenge to op-
timal planning and delivery of radiation doses. Recent de-
velopments in image guided radiotherapy has caused a sound
request for more advanced approaches for image registration
to handle these deformations. Viscous-fluid registration is
one such deformable registration method. A drawback with
this method has been that it has required computation times
that were too long to make the approach clinically appli-
cable. With recent advances in programmability of graph-
ics hardware, complex user defined calculations can now be
performed on consumer graphics cards (GPUs). This pa-
per demonstrates that the GPU can be used to drastically
reduce the time needed to register two medical 3D images
using the viscous-fluid registration method. This facilitates
an increased incorporation of image registration in radio-
therapy treatment of cancer patients, potentially leading to
more efficient treatment with less severe side effects.
Ninth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Aarhus, Denmark, October 20-22, 2008
Authors: Jensen Kurt
Published: February 2016

This booklet contains the proceedings of the Ninth Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, October 20-22, 2008. The workshop is organised by the CPN group at the Department of Computer Science, University of Aarhus, Denmark. The papers are also available in electronic form via the web pages: http://www.daimi.au.dk/CPnets/workshop08
First-Class Object Sets
Authors: Ernst Erik
Published: February 2016

Abstract. Typically, objects are monolithic entities with a fixed interface. To increase the flexibility in this area, this paper presents first-class object sets as a language construct. An object set offers an interface which is a disjoint union of the interfaces of its member objects. It may also be used for a special kind of method invocation involving multiple
objects in a dynamic lookup process. With support for feature access and late-bound method calls object sets are similar to ordinary objects, only more flexible. The approach is made precise by means of a small calculus, and the soundness of its type system is shown by a mechanically checked proof in Coq.
Tenth Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools Aarhus, Denmark, October 19-21, 2009
Authors: Jensen Kurt
Published: February 2016

This booklet contains the proceedings of the Tenth Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, October 19-21, 2009. The workshop is organised by the CPN group at the Department of Computer Science, University of Aarhus, Denmark. The papers are also available in electronic form via the web pages: http://www.cs.au.dk/CPnets/events/workshop09
DHRS 2009 Proceedings of the Ninth Danish Human-Computer Interaction Research Symposium.
Authors: Bertelsen Olav , Kanstrup Anne Marie
Published: February 2016

Since 2001 the annual Danish Human-Computer Interaction Research Symposium has been a platform for networking, and provided an opportunity to get an overview across the various parts of the Danish HCI research scene. This years symposium was held in Aarhus, Denmark on December 14, 2009
Proceedings of Therapeutic Strategies A Challenge for User Involvement in Design Workshop in conjunction with NORDICHI 2010 17. October 2010, Reykjavik, Iceland
Authors: Bertelsen Olav , Fitzpatrick Geraldine , Höök Kristina , Balaam Madeline , Grönvall Erik
Published: February 2016
TinyDebug: Multi-Purpose Passive Debugging Framework for Embedded Wireless Systems
Authors: Hansen Morten Tranberg
Published: February 2016

Debugging embedded wireless systems can be cumbersome

due to low visibility. To ease the task of debugging this

paper present TinyDebug which is a multi-purpose passive

debugging framework for developing embedded wireless sys-

tems. TinyDebug is designed to be used throughout the

entire system development process, ranging from simulation

to actual deployment. TinyDebug provides out-of-the-box

message oriented debugging and event logging mechanism

while enabling more advanced debugging techniques to pro-

cess the same debug events.

We present the TinyDebug framework with all its features

from event logging to extraction and show how the frame-

work improves upon existing message based and event log-

ging debugging techniques while enabling distributed event

processing. We also present a number of optional event anal-

ysis tools demon