bluuebunny/crossref_metadata_2025 huggingface dataset:
Optimal Time-Space Trade-Offs for Sorting
Authors: Pagter Jakob , Rauhe Theis
Published: February 2016

We study the fundamental problem of sorting in a sequential model of computation and in particular consider the time-space trade-off (product of time and space) for this problem.
Beame has shown a lower bound of  Omega(n^2) for this product leaving a gap of a logarithmic factor up to the previously best known upper bound of O(n^2 log n) due to Frederickson. Since then, no progress has been made towards tightening this gap.
The main contribution of this paper is a comparison based sorting algorithm which closes this gap by meeting the lower bound of Beame. The time-space product O(n^2) upper bound holds for the full range of space bounds between log n and n/log n. Hence in this range our algorithm is optimal for comparison based models as well as for the very powerful general models considered by Beame.
Compiling Actions by Partial Evaluation, Revisited
Authors: Danvy Olivier , Rhiger Morten
Published: February 2016

We revisit Bondorf and Palsberg's compilation of actions using< the offline syntax-directed partial evaluator Similix (FPCA'93, JFP'96), and we compare it in detail with using an online type-directed partial evaluator. In contrast to Similix, our type-directed partial evaluator is idempotent and requires no "binding-time improvements." It also appears to consume about 7 times less space and to be about 28 times faster than Similix, and to yield residual programs that are perceptibly more efficient than those generated by Similix.
Marked Ancestor Problems
Authors: Alstrup Stephen , Husfeldt Thore , Rauhe Theis
Published: February 2016

Full text not available.
 [Extended abstract appears in Motwani, editor, 39th Annual Symposium on Foundations of Computer Science, FOCS '98 Proceedings, 1998, pages 534-543.]
A Comparison of Petri Net Semantics under the Collective Token Philosophy
Authors: Bruni Roberto , Meseguer José , Montanari Ugo , Sassone Vladimiro
Published: February 2016

In recent years, several semantics for place/transition Petri nets have been proposed that adopt the collective token philosophy. We investigate distinctions and similarities between three such models, namely configuration structures, concurrent transition systems, and (strictly) symmetric (strict) monoidal categories. We use the notion of adjunction to express each connection. We also present a purely logical description of the collective token interpretation of net behaviours in terms of theories and theory morphisms in partial membership equational logic.
Things that can and things that can’t be done in PRA
Authors: Kohlenbach Ulrich
Published: February 2016

It is well-known by now that large parts of (non-constructive) mathematical reasoning can be carried out in systems T which are conservative over primitive recursive arithmetic PRA (and even much weaker systems). On the other hand there are principles S of elementary analysis (like the Bolzano-Weierstrass principle, the existence of a limit superior for bounded sequences etc.) which are known to be equivalent to arithmetical
comprehension (relative to T ) and therefore go far beyond the strength of PRA (when added to T ).
In this paper we determine precisely the arithmetical and computational strength (in terms of optimal conservation results and subrecursive characterizations of provably recursive functions) of weaker function parameter-free schematic versions S− of S, thereby
exhibiting different levels of strength between these principles as well as a sharp borderline between fragments of analysis which are still conservative over PRA and extensions which just go beyond the strength of PRA.
A Categorical Axiomatics for Bisimulation
Authors: Cattani Gian Luca , Power John , Winskel Glynn
Published: February 2016

We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. We work with 2-monads, T, on Cat. Operations on processes, such as nondeterministic sum, prexing and parallel composition are modelled using functors in the Kleisli category for the 2-monad T. We may define the notion of open map for any such 2-monad; in examples of interest, that agrees exactly with the usual notion of functional bisimulation. Under a condition on T, namely that it be a dense KZ-monad, which we define, it follows that functors in Kl(T) preserve open maps, i.e., they respect functional bisimulation. We further
investigate structures on Kl(T) that exist for axiomatic reasons,
primarily because T is a dense KZ-monad, and we study how those structures help to model operations on processes. We outline how this analysis gives ideas for modelling higher order processes. We conclude by making comparison with the use of presheaves and profunctors to model process calculi.
Martingales and Locality in Distributed Computing
Authors: Dubhashi Devdatt P.
Published: February 2016

We use Martingale inequalities to give a simple and uniform analysis of two families of distributed randomised algorithms for edge colouring graphs.
Talagrand’s Inequality and Locality in Distributed Computing
Authors: Dubhashi Devdatt P.
Published: February 2016

We illustrate the use of Talagrand's inequality and an extension
of it to dependent random variables due to Marton for the analysis
of distributed randomised algorithms, specifically, for edge colouring
graphs.
Talagrand’s Inequality in Hereditary Settings
Authors: Dubhashi Devdatt P.
Published: February 2016

We develop a nicely packaged form of Talagrand's inequality that
can be applied to prove concentration of measure for functions defined by hereditary properties. We illustrate the framework with several applications from combinatorics and algorithms. We also give an extension of the inequality valid in spaces satisfying a certain negative dependence property and give some applications.
Comparison of Coding DNA
Authors: Pedersen Christian N. S. , Lyngsø Rune B. , Hein Jotun
Published: February 2016

We discuss a model for the evolutionary distance between two coding DNA sequences which specializes to the DNA/protein model proposed in Hein [3]. We discuss the DNA/protein model in details and present a quadratic time algorithm that computes an optimal alignment of two coding DNA sequences in the model under the assumption of affine gap cost. The algorithm solves a conjecture in [3] and we believe that the constant factor of the running time is sufficiently small to make the algorithm feasible in practice.
Verifiable Encryption and Applications to Group Signatures and Signature Sharing
Authors: Camenisch Jan , Damgård Ivan B.
Published: February 2016

We generalise and improve the security and efficiency of the verifiable encryption scheme of Asokan et al., such that it can rely on more general assumptions, and can be proven secure without relying on random oracles. We show a new application of verifiable encryption to group signatures with separability, these schemes do not need special purpose keys but can work with a wide range of signature and encryption schemes already in use. Finally, we extend our basic primitive to verifiable threshold and group encryption. By encrypting digital signatures this way, one gets new solutions to the verifiable signature sharing problem.
Efficient Multiparty Computations with Dishonest Minority
Authors: Cramer Ronald , Damgård Ivan B. , Dziembowski Stefan , Hirt Martin , Rabin Tal
Published: February 2016

We consider verifiable secret sharing (VSS) and multiparty computation (MPC) in the secure channels model, where a broadcast channel is given and a non-zero error probability is allowed. In this model Rabin and Ben-Or proposed VSS and MPC protocols, secure against an adversary that can corrupt any minority of the players. In this paper, we rst observe that a subprotocol of theirs, known as weak secret sharing (WSS), is not secure against an adaptive adversary, contrary to what was believed earlier. We then propose new and adaptively secure protocols for WSS, VSS and MPC that are substantially more efficient than the original ones. Our protocols generalize easily to provide security against general Q2 adversaries.
An n-ary zipWith in Haskell
Authors: Fridlender Daniel , Indrika Mia
Published: February 2016

The aim of this note is to present an alternative definition of the
zipWith family in the Haskell Library Report [5]. Because of the difficulties in defining a well-typed function with a variable number of arguments, [5] presents a family of zipWith functions. It provides zip functions zipWith2, zipWith3, . . . , zipWith7. For each n, zipWithn zips n lists with a n-ary function. Defining a single zipWith function with a variable number of arguments seems to require dependent types. Inspired by [3], we show, however, how to define such a function in Haskell by means of a binary operator for grouping its arguments. For comparison, we also give definitions of zipWith in languages with dependent types.
An Interpretation of the Fan Theorem in Type Theory
Authors: Fridlender Daniel
Published: February 2016

This article presents a formulation of the fan theorem in
Martin-L¨of's type theory. Starting from one of the standard versions of the fan theorem we gradually introduce reformulations leading to a final version which is easy to interpret in type theory. Finally we describe a formal proof of that final version of the fan theorem.

Keywords: type theory, fan theorem, inductive bar.
Towards Re-usable Real-Time Objects
Authors: Nielsen Brian , Agha Gul
Published: February 2016

Large and complex real-time systems can benefit significantly
from a component-based development approach where new systems are constructed by composing reusable, documented and previously tested concurrent objects. However, reusing objects which execute under real-time constraints is problematic because application specific time and synchronization constraints are often embedded in the internals of these objects. The tight coupling of functionality and real-time constraints makes objects interdependent, and as a result difficult to reuse in another system. We propose a model which facilitates separate and modular specification of real-time constraints, and show how separation of real-time constraints and functional behavior is possible. We present our ideas using the Actor model to represent untimed objects, and the Real-time Synchronizers language to express real-time and synchronization constraints. We discuss specific mechanisms by which Real-time Synchronizers can govern the interaction and execution of untimed objects.
We treat our model formally, and succinctly define what effect
real-time constraints have on a set of concurrent objects. We
briefly discuss how a middleware scheduling and event-dispatching service can use the synchronizers to execute the system.
Clock Difference Diagrams
Authors: Larsen Kim G. , Weise Carsten , Yi Wang , Pearson Justin
Published: February 2016

We sketch a BDD-like structure for representing unions of simple convex polyhedra, describing the legal values of a set of clocks given bounds on the values of clocks and clock dffierences.
The Power of Reachability Testing for Timed Automata
Authors: Aceto Luca , Bouyer Patricia , Burgueno Augusto , Larsen Kim G.
Published: February 2016

In this paper we provide a complete characterization of the class of
properties of (networks of) timed automata for which model checking can be reduced to reachability checking in the context of testing automata.
A Cook’s Tour of Equational Axiomatizations for Prefix Iteration
Authors: Aceto Luca , Fokkink Willem Jan , Ingólfsdóttir Anna
Published: February 2016

Prefix iteration is a variation on the original binary version of the
Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action, and yields simple iterative behaviours that can be equationally characterized by means of finite collections of axioms. In this paper, we present axiomatic characterizations for a significant fragment of the notions of equivalence and preorder in van Glabbeek's linear-time/branching-time spectrum over Milner's basic CCS extended with prefix iteration. More precisely, we consider ready simulation, simulation, readiness, trace and language semantics, and provide complete (in)equational axiomatizations for each of these notions over BCCS with prefix iteration. All of the axiom systems we present are finite, if so is the set of atomic actions under consideration.
Formatting Strings in ML
Authors: Danvy Olivier
Published: February 2016

A string-formatting function such as printf in C seemingly requires dependent types, because its control string specifies the rest of its arguments.

Examples: printf ("Hello world.\n");
printf (" The %s is %d.\n", "answer", 42);We show how changing the representation of the control string makes it possible to program printf in ML (which does not allow dependent types). The result is well typed and perceptibly more efficient than the corresponding library functions in Standard ML of New Jersey and in Caml.

P.S. See also BRICS-RS-98-12
Automated Modeling of Real-Time Implementation
Authors: Jensen Peter Krogsgaard
Published: February 2016

This paper describes ongoing work on the automatic construction
of formal models from Real-Time implementations. The model construction is based on measurements of the timed behavior of the threads of an implementation, their causal interaction patterns and external visible events. A specification of the timed behavior is modelled in timed automata and checked against the generated model in order to validate their timed behavior.
Imperative Objects and Mobile Processes
Authors: Kleist Josva , Sangiorgi Davide
Published: February 2016

An interpretation of Abadi and Cardelli's first-order Imperative Object
Calculus into a typed pi-calculus is presented. The interpretation
validates the subtyping relation and the typing judgements of the Object
Calculus, and is computationally adequate. The proof of computational
adequacy makes use of (a pi-calculus version) of ready simulation, and of a
factorisation of the interpretation into a functional part and a very simple
imperative part. The interpretation can be used to compare and contrast
the Imperative and the Functional Object Calculi, and to prove properties
about them, within a unified framework.
Hereditary History Preserving Simulation is Undecidable
Authors: Jurdzinski Marcin , Nielsen Mogens
Published: February 2016

We show undecidability of hereditary history preserving simulation
for finite asynchronous transition systems by a reduction from the halting
problem of deterministic Turing machines. To make the proof more
transparent we introduce an intermediate problem of deciding the winner
in domino snake games. First we reduce the halting problem of deterministic
Turing machines to domino snake games. Then we show how to
model a domino snake game by a hereditary history simulation game on
a pair of finite asynchronous transition systems.
On the Uniform Weak König’s Lemma
Authors: Kohlenbach Ulrich
Published: February 2016

The so-called weak K¨onig's lemma WKL asserts the existence of an infinite
path b in any infinite binary tree (given by a representing function f). Based on
this principle one can formulate subsystems of higher-order arithmetic which
allow to carry out very substantial parts of classical mathematics but are PI^0_2-conservative
over primitive recursive arithmetic PRA (and even weaker fragments of arithmetic). In [10] we established such conservation results relative to finite type extensions PRA^omega of PRA (together with a quantifier-free axiom of choice schema). In this setting one can consider also a uniform version UWKL of WKL which asserts the existence of a functional Phi which selects uniformly in a given infinite binary tree f an infinite path Phi f of that tree.
This uniform version of WKL is of interest in the context of explicit mathematics as developed by S. Feferman. The elimination process in [10] actually can be used to eliminate even this uniform weak K¨onig's lemma provided that PRA^omega only has a quantifier-free rule of extensionality QF-ER instead of the full axioms (E) of extensionality for all finite types. In this paper we show that in the presence of (E), UWKL is much stronger than WKL: whereas WKL remains to be Pi^0_2 -conservative over PRA, PRA^omega +(E)+UWKL contains (and is conservative over) full Peano arithmetic PA.
Finding Maximal Pairs with Bounded Gap
Authors: Brodal Gerth Stølting , Lyngsø Rune B. , Pedersen Christian N. S. , Stoye Jens
Published: February 2016

A pair in a string is the occurrence of the same substring twice. A pair
is maximal if the two occurrences of the substring cannot be extended to
the left and right without making them different. The gap of a pair is
the number of characters between the two occurrences of the substring.
In this paper we present methods for finding all maximal pairs under
various constraints on the gap. In a string of length n we can find all
maximal pairs with gap in an upper and lower bounded interval in time
O(n log n + z) where z is the number of reported pairs. If the upper
bound is removed the time reduces to O(n+z). Since a tandem repeat is
a pair where the gap is zero, our methods can be seen as a generalization
of finding tandem repeats. The running time of our methods equals the
running time of well known methods for finding tandem repeats.
Protein Folding in the 2D HP Model
Authors: Lyngsø Rune B. , Pedersen Christian N. S.
Published: February 2016

We study folding algorithms in the two-dimensional Hydrophobic-
Hydrophilic model (2D HP model) for protein structure formation. We
consider three generalizations of the best known approximation algorithm.
We show that two of the generalizations do not improve the worst
case approximation ratio. The third generalization seems to be better,
and the analysis of its approximation ratio leads to an interesting combinatorial
problem.
A Semantic Account of Type-Directed Partial Evaluation
Authors: Filinski Andrzej
Published: February 2016

We formally characterize partial evaluation of functional programs
 as a normalization problem in an equational theory, and derive
a type-based normalization-by-evaluation algorithm for computing
normal forms in this setting. We then establish the correctness
 of this algorithm using a semantic argument based on Kripke
logical relations. For simplicity, the results are stated for a non-
strict, purely functional language; but the methods are directly
applicable to stating and proving correctness of type-directed partial
evaluation in ML-like languages as well.
A Note on Spector’s Quantifier-Free Rule of Extensionality
Authors: Kohlenbach Ulrich
Published: February 2016

In this note we show that the so-called weakly extensional arithmetic
in all finite types, which is based on a quantifier-free rule of
extensionality due to C. Spector and which is of significance in the
context of G¨odel's functional interpretation, does not satisfy the deduction
theorem for additional axioms. This holds already for PI^0_1-
axioms. Previously, only the failure of the stronger deduction theorem
for deductions from (possibly open) assumptions (with parameters
kept fixed) was known.
On proving syntactic properties of CPS programs
Authors: Danvy Olivier , Dzafic Belmina , Pfenning Frank
Published: February 2016

Higher-order program transformations raise new challenges for proving
properties of their output, since they resist traditional, first-order proof
techniques. In this work, we consider (1) the "one-pass" continuation-passing
style (CPS) transformation, which is second-order, and (2) the
occurrences of parameters of continuations in its output. To this end, we
specify the one-pass CPS transformation relationally and we use the proof
technique of logical relations.
Finding Maximal Quasiperiodicities in Strings
Authors: Brodal Gerth Stølting , Pedersen Christian N. S.
Published: February 2016

Apostolico and Ehrenfeucht defined the notion of a maximal quasiperiodic
substring and gave an algorithm that finds all maximal quasiperiodic
substrings in a string of length n in time O(n log2 n). In this paper we
give an algorithm that finds all maximal quasiperiodic substrings in a
string of length n in time O(n log n) and space O(n). Our algorithm uses
the suffix tree as the fundamental data structure combined with efficient
methods for merging and performing multiple searches in search trees.
Besides finding all maximal quasiperiodic substrings, our algorithm also
marks the nodes in the suffix tree that have a superprimitive path-label.
An Expressive Extension of TLC
Authors: Henriksen Jesper G.
Published: February 2016

A temporal logic of causality (TLC) was introduced by Alur, Penczek
and Peled in [1]. It is basically a linear time temporal logic
interpreted over Mazurkiewicz traces which allows quantification over
causal chains. Through this device one can directly formulate causality
properties of distributed systems. In this paper we consider an
extension of TLC by strengthening the chain quantification operators.
We show that our logic TLC  adds to the expressive power of TLC.
We do so by defining an Ehrenfeucht-Fraissé game to capture the expressive
 power of TLC. We then exhibit a property and by means of
this game prove that the chosen property is not definable in TLC. We
then show that the same property is definable in TLC. We prove in
fact the stronger result that TLC is expressively stronger than TLC
exactly when the dependence relation associated with the underlying
trace alphabet is not transitive.
Wavelet Based 3D Compression for Very Large Volume Data Supporting Fast Random Access
Authors: Rodler Flemming Friche
Published: February 2016

We propose a wavelet based method for compressing volumetric
 data with little loss in quality. The method supports fast
random access to individual voxels within the compressed volume.
 Such a method is important since storing and visualising
very large volumes impose heavy demands on internal memory
and external storage facilities making it accessible only to users
with huge and expensive computers. This problem is not likely to
become less in the future. Experimental results on the CT dataset
of the Visible Human have shown that our method provides very
high compression rates with fairly fast random access.
Presheaf Models for CCS-like Languages
Authors: Cattani Gian Luca , Winskel Glynn
Published: February 2016

The aim of this paper is to harness the mathematical machinery around
presheaves for the purposes of process calculi. Joyal, Nielsen and Winskel
proposed a general definition of bisimulation from open maps. Here we show
that open-map bisimulations within a range of presheaf models are congruences
 for a general process language, in which CCS and related languages
are easily encoded. The results are then transferred to traditional models
 for processes. By first establishing the congruence results for presheaf
models, abstract, general proofs of congruence properties can be provided
and the awkwardness caused through traditional models not always possessing
 the cartesian liftings, used in the break-down of process operations,
are side-stepped. The abstract results are applied to show that hereditary
history-preserving bisimulation is a congruence for CCS-like languages to
which is added a refinement operator on event structures as proposed by
van Glabbeek and Goltz.
Linear Time Recognition of P4-Indifferent Graphs
Authors: Rizzi Romeo
Published: February 2016

A simple graph is P4-indifferent if it admits a total order < on
its nodes such that every chordless path with nodes a, b, c, d and edges
ab, bc, cd has a < b < c < d or a > b > c > d. P4-indifferent graphs generalize
 indifferent graphs and are perfectly orderable. Recently, Hoang,
Maray and Noy gave a characterization of P4-indifferent graphs in
terms of forbidden induced subgraphs. We clarify their proof and describe
 a linear time algorithm to recognize P4-indifferent graphs. When
the input is a P4-indifferent graph, then the algorithm computes an order < as above.

Key words: P4-indifference, linear time, recognition, modular decomposition.

 
On Plain and Hereditary History-Preserving Bisimulation
Authors: Fröschle Sibylle B. , Hildebrandt Thomas Troels
Published: February 2016

We investigate the difference between two well-known notions of
independence bisimilarity, history-preserving bisimulation and hereditary
history-preserving bisimulation. We characterise the difference between
the two bisimulations in trace-theoretical terms, advocating the
view that the first is (just) a bisimulation for causality, while the second
is a bisimulation for concurrency. We explore the frontier zone between
the two notions by defining a hierarchy of bounded backtracking bisimulations.
Our goal is to provide a stepping stone for the solution to
the intriguing open problem of whether hereditary history-preserving
bisimulation is decidable or not. We prove that each of the bounded
bisimulations is decidable. However, we also prove that the hierarchy
is strict. This rules out the possibility that decidability of the general
problem follows directly from the special case. Finally, we give a non-
trivial reduction solving the general problem for a restricted class of
systems and give pointers towards a full answer.
Super-Polynomial Versus Half-Exponential Circuit Size in the Exponential Hierarchy
Authors: Miltersen Peter Bro , Variyam Vinodchandran N. , Watanabe Osamu
Published: February 2016

Lower bounds on circuit size were previously established for functions
 in Sigma^p_2, ZPP^NP, Sigma^exp_2, ZPEXP^NP and MA_exp. We investigate
the general question: Given a time bound f(n). What is the best circuit
 size lower bound that can be shown for the classes MA-TIME[f],
ZP-TIME^NP[f], . . . using the techniques currently known? For the
classes MA_exp, ZPEXP^NP, and Sigma^exp_2 , the answer we get is
"half-exponential". Informally, a function f is said to be half-exponential if
f composed with itself is exponential
Faster Deterministic Dictionaries
Authors: Pagh Rasmus
Published: February 2016

We consider static dictionaries over the universe U = {0, 1}^w on a
unit-cost RAM with word size w. Construction of a static dictionary with
linear space consumption and constant lookup time can be done in linear
expected time by a randomized algorithm. In contrast, the best previous
deterministic algorithm for constructing such a dictionary with n elements
runs in time O(n^(1+epsilon)) for epsilon > 0. This paper narrows the gap between
deterministic and randomized algorithms exponentially, from the factor of
n^epsilon to an O(log n) factor. The algorithm is weakly non-uniform, i.e. requires
certain precomputed constants dependent on w. A by-product of the result
is a lookup time vs insertion time trade-off for dynamic dictionaries, which
is optimal for a certain class of deterministic hashing schemes.
Observational Mu-Calculus
Authors: Bradfield Julian C. , Stevens Perdita
Published: February 2016

We propose an extended modal mu-calculus to provide an `assembly
language' for modal logics for real time, value-passing calculi,
and other extended models of computation.
Towards a Theory of Regular MSC Languages
Authors: Henriksen Jesper G. , Mukund Madhavan , Kumar K. Narayan , Thiagarajan P. S.
Published: February 2016

Message Sequence Charts (MSCs) are an attractive visual formalism
 widely used to capture system requirements during the early
design stages in domains such as telecommunication software. It is
fruitful to have mechanisms for specifying and reasoning about
collections of MSCs so that errors can be detected even at the requirements
 level. We propose, accordingly, a notion of regularity for
collections of MSCs and explore its basic properties. In particular, we
provide an automata-theoretic characterization of regular MSC
languages in terms of finite-state distributed automata called bounded
message-passing automata. These automata consist of a set of
sequential processes that communicate with each other by sending and
receiving messages over bounded FIFO channels. We also provide a
logical characterization in terms of a natural monadic second-order
logic interpreted over MSCs.
A commonly used technique to generate a collection of MSCs is
to use a Message Sequence Graph (MSG). We show that the class of
languages arising from the so-called locally synchronized MSGs constitute
 a proper subclass of the languages which are regular in our sense.
In fact, we characterize the locally synchronized MSG languages as
the subclass of regular MSC languages that are finitely generated.
Logical Specification of Operational Semantics
Authors: Mosses Peter D.
Published: February 2016

Various logic-based frameworks have been proposed for
specifying the operational semantics of programming languages and
concurrent systems, including inference systems in the styles advocated by
Plotkin and by Kahn, Horn logic, equational specifications, reduction
systems for evaluation contexts, rewriting logic, and tile logic.
We consider the relationship between these frameworks, and assess their
respective merits and drawbacks - especially with regard to the modularity
 of specifications, which is a crucial feature for scaling up to practical
applications. We also report on recent work towards the use of the Maude
system (which provides an efficient implementation of rewriting logic) as
a meta-tool for operational semantics.
Event Structures as Presheaves —Two Representation Theorems
Authors: Winskel Glynn
Published: February 2016

The category of event structures is known to embed fully
and faithfully in the category of presheaves over pomsets. Here a characterisation
of the presheaves represented by event structures is presented.
The proof goes via a characterisation of the presheaves represented by
event structures when the morphisms on event structures are "strict" in
that they preserve the partial order of causal dependence.
A Runtime System for Interactive Web Services
Authors: Brabrand Claus , Møller Anders , Sandholm Anders B. , Schwartzbach Michael I.
Published: February 2016

Interactive web services are increasingly replacing traditional static
web pages. Producing web services seems to require a tremendous
amount of laborious low-level coding due to the primitive nature of
CGI programming. We present ideas for an improved runtime system
for interactive web services built on top of CGI running on virtually
every combination of browser and HTTP/CGI server. The runtime
system has been implemented and used extensively in , a
tool for producing interactive web services.

Keywords: CGI, Interactive Web Service, Web Document Management,
Runtime System, Session Model.
Intuitionistic Choice and Restricted Classical Logic
Authors: Kohlenbach Ulrich
Published: February 2016

Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic
in all finite types together with various forms of the axiom of choice and
a numerical omniscience schema (NOS) which implies classical logic for arithmetical
formulas. Feferman subsequently observed that the proof theoretic
strength of such systems can be determined by functional interpretation based
on a non-constructive mu-operator and his well-known results on the strength
of this operator from the 70's.
In this note we consider a weaker form LNOS (lesser numerical omniscience
schema) of NOS which suffices to derive the strong form of binary K¨onig's
lemma studied by Coquand/Palmgren and gives rise to a new and mathematically
strong semi-classical system which, nevertheless, can proof theoretically
be reduced to primitive recursive arithmetic PRA. The proof of this fact relies
on functional interpretation and a majorization technique developed in a
previous paper.
A Note on NP intersection coNP/poly
Authors: Variyam Vinodchandran N.
Published: February 2016

In this note we show that AMexp is not in NP intersection coNP/poly, where
AMexp denotes the exponential version of the class AM. The main
part of the proof is a collapse of EXP to AM under the assumption
that EXP is in NP intersection coNP/poly
Using Automata in Control Synthesis. A Case Study
Authors: Hune Thomas S. , Sandholm Anders B.
Published: February 2016

We study a method for synthesizing control programs. The
method merges an existing control program with a control automaton.
For specifying the control automata we have used monadic second order
logic over strings. Using the Mona tool, specifications are translated into
automata. This yields a new control program restricting the behavior of
the old control program such that the specifications are satisfied. The
method is presented through a concrete example.
Continuous Additive Algebras and Injective Simulations of Synchronization Trees
Authors: Ésik Zoltán
Published: February 2016

The (in)equational properties of the least fixed point operation on
(omega-)continuous functions on (omega-)complete partially ordered sets are
captured by the axioms of (ordered) iteration algebras, or iteration
theories. We show that the inequational laws of the sum operation in
conjunction with the least fixed point operation in continuous additive
algebras have a finite axiomatization over the inequations of ordered
iteration algebras. As a byproduct of this relative axiomatizability
result, we obtain complete infinite inequational and finite implicational
axiomatizations. Along the way of proving these results, we give a
concrete description of the free algebras in the corresponding variety of
ordered iteration algebras. This description uses injective simulations of
regular synchronization trees. Thus, our axioms are also sound and
complete for the injective simulation (resource bounded simulation) of
(regular) processes.

Keywords: equational logic, fixed points, synchronization trees, simulation.
Modelling and Control of Discrete Event Dynamic Systems
Authors: Capkovic Frantisek
Published: February 2016

Discrete event dynamic systems (DEDS) in general are
investigated as to their analytical models most suitable for control
purposes and as to the analytical methods of the control synthesis.
 The possibility of utilising both the selected kind of Petri nets
and the oriented graphs on this way is pointed out. Because many
times the control task specifications (like criteria, constraints,
special demands, etc.) are given only verbally or in another form of
non analytical terms, a suitable knowledge representation about
the specifications is needed. Special kinds of Petri nets (logical,
fuzzy) are suitable on this way too. Hence, the knowledge-based
control synthesis of DEDS can also be examined. The developed
graphical tools for model drawing and testing as well as for the
automated knowledge-based control synthesis are described and
illustratively presented.
Two approaches to modelling and control synthesis based on
oriented graphs are developed. They are suitable when the
system model is described by the special kind of Petri nets - state
machines. At the control synthesis the first of them is straightforward
 while the second one combines both the straight-lined model
dynamics development (starting from the given initial state
towards the prescribed terminal one) and the backtracking model
dynamics development.
Practical Threshold RSA Signatures Without a Trusted Dealer
Authors: Damgård Ivan B. , Koprowski Maciej
Published: February 2016

We propose a threshold RSA scheme which is as efficient as the fastest previous
threshold RSA scheme (by Shoup), but where two assumptions needed in Shoup's and in
previous schemes can be dropped, namely that the modulus must be a product of safe primes
and that a trusted dealer generates the keys.
Dispersing Hash Functions
Authors: Pagh Rasmus
Published: February 2016

A new hashing primitive is introduced: dispersing hash functions. A family
of hash functions F is dispersing if, for any set S of a certain size and random
h in F, the expected value of |S|−|h[S]| is not much larger than the expectancy
if h had been chosen at random from the set of all functions.
We give tight, up to a logarithmic factor, upper and lower bounds on the
size of dispersing families. Such families previously studied, for example
universal families, are significantly larger than the smallest dispersing families,
making them less suitable for derandomization. We present several applications
 of dispersing families to derandomization (fast element distinctness, set
inclusion, and static dictionary initialization). Also, a tight relationship
between dispersing families and extractors, which may be of independent interest,
is exhibited.
We also investigate the related issue of program size for hash functions
which are nearly perfect. In particular, we exhibit a dramatic increase in
program size for hash functions more dispersing than a random function.
The bigwig Project
Authors: Brabrand Claus , Møller Anders , Schwartzbach Michael I.
Published: February 2016

We present the results of the -bigwig- project, which aims to design and implement a high-level domain-specific language for programming interactive Web services.
The World Wide Web has undergone an extreme development since its invention ten years ago. A fundamental aspect is the 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. Each aspect is handled by a nearly independent sublanguage, and the entire collection is integrated into a common core language. The -bigwig- compiler uses the available Web technologies as target languages, making -bigwig- available on almost any combination of browser and server, without relying on plug-ins or server modules.
The Second Futamura Projection for Type-Directed Partial Evaluation
Authors: Grobauer Bernd , Yang Zhe
Published: February 2016

A generating extension of a program specializes the program with respect to part of the input. Applying a partial evaluator to the program trivially yields a generating extension, but specializing the partial evaluator with respect to the program often yields a more efficient one. This specialization can be carried out by the partial evaluator itself; in this case, the process is known as the second Futamura projection. We derive an ML implementation of the second Futamura projection for Type-Directed Partial Evaluation (TDPE). Due to the differences between `traditional', syntax-directed partial evaluation and TDPE, this derivation involves several conceptual and technical steps. These include a suitable formulation of the second Futamura projection and techniques for making TDPE amenable to self-application. In the context of the second Futamura projection, we also compare and relate TDPE with conventional offline partial evaluation.
We demonstrate our technique with several examples, including
compiler generation for Tiny, a prototypical imperative language.
Reasoning About Code-Generation in Two-Level Languages
Authors: Yang Zhe
Published: February 2016

We show that two-level languages are not only a good tool for describing code-generation algorithms, but a good tool for reasoning about them
as well. Indeed, some general properties of two-level languages capture common proof obligations of code-generation algorithms in the form of two-level programs.

- To prove that the generated code behaves as desired, we use an erasure property, which equationally relates the generated code to an erasure of the original two-level program in the object language, thereby reducing the two-level proof obligation to a simpler one-level obligation.

- To prove that the generated code satisfies certain syntactic constraints, e.g., that it is in some normal form, we use a type-preservation property for a refined type system that enforces these constraints.

In addition, to justify concrete implementations of code-generation algorithms in one-level languages, we use a native embedding of a two-level language into a one-level language. We present two-level languages with these properties both for a call-by-name object language and for a call-by-value object language with computational effects. Indeed, it is these properties that guide our language design in the call-by-value case. We consider two classes of non-trivial applications:
one-pass transformations into continuation-passing style and
type-directed partial evaluation for call-by-name and for call-by-value.

Keywords. Two-level languages, erasure, type preservation, native implementation,
partial evaluation.
Higher Order Reverse Mathematics
Authors: Kohlenbach Ulrich
Published: February 2016

In this paper we argue for an extension of the second order frame-work currently used in the program of reverse mathematics to finite types. In particular we propose a conservative finite type extension RCA^omega_0 of the second order base system RCA_0. By this conservation nothing is lost for second order statements if we reason in RCA^omega_0 in stead of RCA_0. However, the presence of finite types allows to treat various analytical notions in a rather direct way, compared to the encodings needed in RCA_0 which are not always provably faithful in RCA_0. Moreover, the language of finite types allows to treat many more principles and gives rise to interesting extensions of the existing scheme of reverse mathematics. We indicate this by showing that the class of principles equivalent (over RCA^omega_0 ) to Feferman's nonconstructive mu-operator forms a mathematically rich and very robust class. This is closely related to a phenomenon in higher type recursion theory known as Grilliot's trick.
Modularity in Meta-Languages
Authors: Mosses Peter D.
Published: February 2016

A meta-language for semantics has a high degree of modularity
when descriptions of individual language constructs can be formulated independently using it, and do not require reformulation when new constructs are added to the described language. The quest for modularity in semantic meta-languages has been going on for more than two decades. Here, most of the main meta-languages for operational, denotational, and hybrid styles of semantics are compared regarding their modularity. A simple bench-mark is used: describing the semantics of a pure functional language, then extending the described language with references, exceptions, and concurrency constructs. For each style of semantics, at least one of the considered meta-languages appears to provide a high degree of modularity.
CASL for CafeOBJ Users
Authors: Mosses Peter D.
Published: February 2016

Casl is an expressive language for the algebraic specification
of software requirements, design, and architecture. It has been developed by an open collaborative effort called CoFI (Common Framework Initiative for algebraic specification and development). Casl combines the best features of many previous main-stream algebraic specification languages, and it should provide a focus for future research and development in the use of algebraic techniques, as well facilitating interoperability of
existing and future tools. This paper presents Casl for users of the CafeOBJ framework, focusing on the relationship between the two languages. It first considers those constructs of CafeOBJ that have direct counterparts in Casl, and then (briefly) those that do not. It also motivates various Casl constructs
that are not provided by CafeOBJ. Finally, it gives a concise overview of Casl, and illustrates how some CafeOBJ specifications may be expressed in Casl.
Effective Uniform Bounds on the Krasnoselski-Mann Iteration
Authors: Kohlenbach Ulrich
Published: February 2016

This paper is a case study in proof mining applied to non-effective proofs
in nonlinear functional analysis. More specifically, we are concerned with the
fixed point theory of nonexpansive selfmappings f of convex sets C in normed spaces. We study the Krasnoselski iteration as well as more general so-called Krasnoselski-Mann iterations. These iterations converge to fixed points of f only under special compactness conditions and even for uniformly convex
spaces the rate of convergence is in general not computable in f (which is
related to the non-uniqueness of fixed points). However, the iterations yield
approximate fixed points of arbitrary quality for general normed spaces and
bounded C (asymptotic regularity).
In this paper we apply general proof theoretic results obtained in previous
papers to non-effective proofs of this regularity and extract uniform explicit
bounds on the rate of the asymptotic regularity. We start off with the classical
case of uniformly convex spaces treated already by Krasnoselski and show
how a logically motivated modification allows to obtain an improved bound. Already the analysis of the original proof (from 1955) yields an elementary
proof for a result which was obtained only in 1990 with the use of the deep
Browder-G¨ohde-Kirk fixed point theorem. The improved bound from the modified
 proof gives applied to various special spaces results which previously had
been obtained only by ad hoc calculations and which in some case are known
to be optimal.
The main section of the paper deals with the general case of arbitrary normed
spaces and yields new results including a quantitative analysis of a theorem
due to Borwein, Reich and Shafrir (1992) on the asymptotic behaviour of
the general Krasnoselski-Mann iteration in arbitrary normed spaces even for unbounded sets C. Besides providing explicit bounds we also get new qualitative results concerning the independence of the rate of convergence of the norm of that iteration from various input data. In the special case of bounded convex sets, where by well-known results of Ishikawa, Edelstein/O'Brian and Goebel/Kirk the norm of the iteration converges to zero, we obtain uniform
bounds which do not depend on the starting point of the iteration and the
nonexpansive function and the normed space X and, in fact, only depend
on the error epsilon, an upper bound on the diameter of C and some very general information on the sequence of scalars k used in the iteration. Even non-effectively only the existence of bounds satisfying weaker uniformity conditions was known before except for the special situation, where lambda_k := lambda is constant. For the unbounded case, no quantitative information was known so far.
The Abstraction and Instantiation of String-Matching Programs
Authors: Amtoft Torben , Consel Charles , Danvy Olivier , Malmkjær Karoline
Published: February 2016

We consider a naive, quadratic string matcher testing whether a
pattern occurs in a text; we equip it with a cache mediating its access to the
text; and we abstract the traversal policy of the pattern, the cache, and
the text. We then specialize this abstracted program with respect to a
pattern, using the off-the-shelf partial evaluator Similix.
Instantiating the abstracted program with a left-to-right traversal policy
 yields the linear-time behavior of Knuth, Morris and Pratt's string
matcher. Instantiating it with a right-to-left policy yields the linear-time
behavior of Boyer and Moore's string matcher.
Events in Security Protocols
Authors: Crazzolara Federico , Winskel Glynn
Published: February 2016

The events of a security protocol and their causal dependency
can play an important role in the analysis of security properties.
 This insight underlies both strand spaces and the inductive
method. But neither of these approaches builds up the events of
a protocol in a compositional way, so that there is an informal
spring from the protocol to its model. By broadening the models
to certain kinds of Petri nets, a restricted form of contextual nets,
a compositional event-based semantics is given to an economical,
but expressive, language for describing security protocols; so the
events and dependency of a wide range of protocols are determined
 once and for all. The net semantics is formally related to a
transition semantics, strand spaces and inductive rules, as well as
trace languages and event structures, so unifying a range of
approaches, as well as providing conditions under which particular,
more limited, models are adequate for the analysis of protocols.
The net semantics allows the derivation of general properties and
proof principles which are demonstrated in establishing an
authentication property, following a diagrammatic style of proof.