bluuebunny/crossref_metadata_2025 huggingface dataset:
On One-Pass CPS Transformations
Authors: Danvy Olivier , Millikin Kevin , Nielsen Lasse R.
Published: February 2016

We bridge two distinct approaches to one-pass CPS transformations, i.e., CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is independently due to Appel, Danvy and Filinski, and Wand, building on Plotkin's seminal work. The other is non-compositional and based on a reduction semantics for the lambda-calculus, and is due to Sabry and Felleisen. To relate the two approaches, we use three tools: Reynolds's defunctionalization and its left inverse, refunctionalization; a special case of fold-unfold fusion due to Ohori and Sasano, fixed-point promotion; and an implementation technique for reduction semantics due to Danvy and Nielsen, refocusing.

This work is directly applicable to transforming programs into monadic normal form.
Refunctionalization at Work
Authors: Danvy Olivier , Millikin Kevin
Published: February 2016

We present the left inverse of Reynolds's defunctionalization and we show its relevance to programming and to programming languages. We present two methods to put a program that is almost in defunctionalized form into one that is actually in defunctionalized form, and we illustrate them with a recognizer for Dyck words and with Dijkstra's shunting-yard algorithm.
Static Analysis for Event-Based XML Processing
Authors: Møller Anders
Published: February 2016

Event-based processing of XML data - as exemplified by the popular SAX framework - is a powerful alternative to using W3C's DOM or similar tree-based APIs. The event-based approach is particularly superior when processing large XML documents in a streaming fashion with minimal memory consumption.

This paper discusses challenges for creating program analyses for SAX applications. In particular, we consider the problem of statically guaranteeing that a given SAX program always produces only well-formed and valid XML output. We propose an analysis technique based on existing analyses of Servlets, string operations, and XML graphs.
Refunctionalization at Work
Authors: Danvy Olivier , Millikin Kevin
Published: February 2016

We present the left inverse of Reynolds's defunctionalization and we show its relevance to programming and to programming languages. We propose two methods to transform a program that is almost in defunctionalized form into one that is actually in defunctionalized form, and we illustrate them with a recognizer for Dyck words and with Dijkstra's shunting-yard algorithm.
Petri Nets and Bisimulations
Authors: Nielsen Mogens , Winskel Glynn
Published: February 2016

Several categorical relationships (adjunctions) between models for concurrency have been established, allowing the translation of concepts and properties from one model to another. The purpose of the present paper is twofold: firstly to present a central example of such a relationship (a coreflection between asynchronous transition systems and Petri nets), and secondly to illustrate its use by transferring to nets a general concept of bisimulation.
External-Storage Data Structures for Plane-Sweep Algorithms
Authors: Arge Lars
Published: February 2016

In this paper we develop a technique for transforming an internal memory datastructure into an external storage data structure suitable for plane-sweep algorithms. We use this technique to develop external storage versions of the range tree and the segment tree. We also obtain an external priority queue. Using the first two structures, we solve the orthogonal segment intersection, the isothetic rectangle intersection, and the batched range searching problem in the optimal number of I/O-operations. Unlike previously known I/O-algorithms the developed algorithms are straightforward generalizations of the ordinary internal memory plane-sweep algorithms. Previously almost no dynamic data structures were known for the model we are working in.
LCF Examples in HOL
Authors: Agerholm Sten
Published: February 2016

The LCF system provides a logic of fixed point theory and is useful to reason about non-termination, arbitrary recursive definitions and infinite types as lazy lists. It is unsuitable for reasoning about finite types and strict functions. The HOL system provides set theory and supports reasoning about finite types and total functions well. In this paper a number of examples are used to demonstrate that an extension of HOL with domain theory combines the benefits of both systems. The examples illustrate reasoning about infinite values and non-terminating functions and show how mixing domain and set theoretic reasoning eases reasoning about finite LCF types and strict functions. An example presents a proof of the correctness and termination of a recursive unification algorithm using well-founded induction.
An Action Semantics for ML Concurrency Primitives
Authors: Mosses Peter D. , Musicante Martín
Published: February 2016

This paper is about the recently-developed framework of action semantics. The pragmatic qualities of action semantic descriptions are particularly good, which encourages their use in industrial-scale applications where semantic descriptions are needed, e.g., compiler development.

The paper has two main aims: to demonstrate the remarkable extensibility of action semantic descriptions, and to illustrate the action semantics treatment of concurrency. These aims are achieved simultaneously, by first giving the description of a sequential (ML-like) programming language fragment, and then extending the described language with some concurrency primitives (taken from CML). The action semantic description of the sequential part of the language does not change at all when the concurrency primitives are added, it merely gets augmented by the description of the new features!
A General Adequacy Result for a Linear Functional Language
Authors: Braüner Torben
Published: February 2016

A main concern of the paper will be a Curry-Howard interpretation of Intuitionistic Linear Logic. It will be extended with recursion, and the resulting functional programming language will be given operational as well as categorical semantics. The two semantics will be related by soundness and adequacy results. The main features of the categorical semantics are that convergence/divergence behaviour is modelled by a strong monad, and that recursion is modelled by ``linear fixpoints'' induced by CPO structure on the hom-sets. The ``linear fixpoints'' correspond to ordinary fixpoints in the category of free coalgebras w.r.t. the comonad used to interpret the ``of course'' modality. Concrete categories from (stable) domain theory satisfying the axioms of the categorical model are given, and thus adequacy follows in these instances from the general result.
Finitisation in Bounded Arithmetic
Authors: Riis Søren
Published: February 2016

I prove various results concerning un-decidability in weak fragments of Arithmetic. All results are concerned with S^{1}_{2} \subseteq T^{1}_{2} \subseteq S^{2}_{2} \subseteq T^{2}_{2} \subseteq.... a hierarchy of theories which have already been intensively studied in the literature. Ideally one would like to separate these systems. However this is generally expected to be a very deep problem, closely related to some of the most famous and open problems in complexity theory.

In order to throw some light on the separation problems, I consider the case where the underlying language is enriched by extra relation and function symbols. The paper introduces a new type of results. These state that the first three levels in the hierarchy (i.e. S^{1}_{2}, T^{1}_{2} and S^{2}_{2}) are never able to distinguish (in a precise sense) the "finite'' from the "infinite''. The fourth level (i.e. T^{2}_{2}) in some cases can make such a distinction. More precisely, elementary principles from finitistical combinatorics (when expressed solely by the extra relation and function symbols) are only provable on the first three levels if they are valid when considered as principles of general (infinitistical) combinatorics. I show that this does not hold for the fourth level.

All results are proved by forcing.
Probabilistic Proof Systems
Authors: Goldreich Oded
Published: February 2016

Various types of probabilistic proof systems have played a central role in the development of computer science in the last decade. In this exposition, we concentrate on three such proof systems -- interactive proofs, zero-knowledge proofs, and probabilistic checkable proofs -- stressing the essential role of randomness in each of them.

This exposition is an expanded version of a survey written for the proceedings of the International Congress of Mathematicians (ICM94) held in Zurich in 1994. It is hope that this exposition may be accessible to a broad audience of computer scientists and mathematians.
Fully Dynamic Transitive Closure in Plane Dags with one Source and one Sink
Authors: Husfeldt Thore
Published: February 2016

We give an algorithm for the Dynamic Transitive Closure Problem for planar directed acyclic graphs with one source and one sink. The graph can be updated in logarithmic time under arbitrary edge insertions and deletions that preserve the embedding. Queries of the form `is there a directed path from u to v ?' for arbitrary vertices u and v can be answered in logarithmic time. The size of the data structure and the initialisation time are linear in the number of edges.

The result enlarges the class of graphs for which a logarithmic (or even polylogarithmic) time dynamic transitive closure algorithm exists. Previously, the only algorithms within the stated resource bounds put restrictions on the topology of the graph or on the delete operation. To obtain our result, we use a new characterisation of the transitive closure in plane graphs with one source and one sink and introduce new techniques to exploit this characterisation.

We also give a lower bound of Omega(log n/log log n) on the amortised complexity of the problem in the cell probe model with logarithmic word size. This is the first dynamic directed graph problem with almost matching lower and upper bounds.
Decidability of Systems of Set Constraints with Negative Constraints
Authors: Aiken Alexander , Kozen Dexter , Wimmers Ed
Published: February 2016

Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general systems of positive set constraints have appeared. In this paper we consider systems of mixed positive and negative constraints, which are considerably more expressive than positive constraints alone. We show that it is decidable whether a given such system has a solution. The proof involves a reduction to a number-theoretic decision problem that may be of independent interest.
On provably disjoint NP-pairs
Authors: Razborov Alexander A.
Published: February 2016

In this paper we study the pairs (U,V) of disjoint NP-sets representable in a theory T of Bounded Arithmetic in the sense that T proves U intersection V = \emptyset. For a large variety of theories T we exhibit a natural disjoint NP-pair which is complete for the class of disjoint NP-pairs representable in T. This allows us to clarify the approach to showing independence of central open questions in Boolean complexity from theories of Bounded Arithmetic initiated in [1]. Namely, in order to prove the independence result from a theory T, it is sufficient to separate the corresponding complete NP-pair by a (quasi)poly-time computable set. We remark that such a separation is obvious for the theory S(S_2) + S Sigma^b_2 - PIND considered in [1], and this gives an alternative proof of the main result from that paper.

[1] A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of Bounded Arithmetic. To appear in Izvestiya of the RAN, 1994.
Fibrations and Calculi of Fractions
Authors: Oosten Jaap Van
Published: February 2016

Given a fibration E -> B and a class Sigma of arrows of B, one can construct the free fibration (on E over B such that all reindexing functors over elements of Sigma are equivalences.

In this work I give an explicit construction of this, and study its properties. For example, the construction preserves the property of being fibrewise discrete, and it commutes up to equivalence with fibrewise exact completions. I show that mathematically interesting situations are examples of this construction. In particular, subtoposes of the effective topos are treated.
CPO Models for GSOS Languages - Part I: Compact GSOS Languages
Authors: Aceto Luca
Published: February 2016

In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail and Meyer. The canonical model used for this purpose will be Abramsky's domain of synchronization trees, and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder. In the process of establishing the full abstraction result, we also obtain several general results on the bisimulation preorder (including a complete axiomatization for it), and give a novel operational interpretation of GSOS languages.
Bistructures, Bidomains and Linear Logic
Authors: Plotkin Gordon , Winskel Glynn
Published: February 2016

Bistructures are a generalisation of event structures to represent spaces of functions at higher types; the partial order of causal dependency is replaced by two orders, one associated with input and the other output in the behaviour of functions. Bistructures form a categorical model of Girard's classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has associated co-Kleisli category which is equivalent to a cartesian-closed full subcategory of Berry's bidomains.
Transforming Comparison Model Lower Bounds to the PRAM
Authors: Breslauer Dany , Dubhashi Devdatt P.
Published: February 2016

This note provides general transformations of lower bounds in Valiant's
parallel comparison decision tree model to lower bounds in the priority
concurrent-read concurrent-write parallel-random-access-machine model.
The proofs rely on standard Ramsey-theoretic arguments that simplify
the structure of the computation by restricting the input domain. The
transformation of comparison model lower bounds, which are usually easier
to obtain, to the parallel-random-access-machine, unifies some known
lower bounds and gives new lower bounds for several problems.
The Girard Translation Extended with Recursion
Authors: Braüner Torben
Published: February 2016

This paper extends Curry-Howard interpretations of Intuitionistic Logic (IL) and Intuitionistic Linear Logic (ILL) with rules for recursion. The resulting term languages, the rec-calculus and the linear rec-calculus respectively, are given sound
categorical interpretations. The embedding of proofs of IL into proofs of ILL given by the Girard Translation is extended with the rules for recursion, such that an embedding of terms of the rec-calculus into terms of the linear rec-calculus is induced via the extended Curry-Howard isomorphisms. This embedding is shown to be sound with respect to the categorical interpretations.

Full version of paper to appear in Proceedings of CSL '94, LNCS 933, 1995.
Optimal Parallel Construction of Minimal Suffix and Factor Automata
Authors: Breslauer Dany , Hariharan Ramesh
Published: February 2016

This paper gives optimal parallel algorithms for the construction of the smallest deterministic finite automata recognizing all the suffixes and the factors of a string. The algorithms use recently discovered optimal parallel suffix tree construction algorithms together with data structures for the efficient manipulation of trees, exploiting the well known relation between suffix and factor automata and suffix trees.
Design Architectures through Category Constraints
Authors: Koistinen Jari , Klarlund Nils , Schwartzbach Michael I.
Published: February 2016

We provide a rigorous and concise formalism for specifying design
architectures exterior to the design language. This allows several
evolving architectural styles to be supported independently. Such architectural
styles are specified in a tailored parse tree logic, which permits
automatic support for conformance and consistency. We exemplify
these ideas with a small design architecture inspired by real world constraints
found in the Ericsson ATM Broadband System.
Compositional Model Checking of Real Time Systems
Authors: Laroussinie Francois , Larsen Kim G.
Published: February 2016

A major problem in applying model checking to finite-state systems
is the potential combinatorial explosion of the state space arising from
parallel composition. Solutions of this problem have been attempted for
practical applications using a variety of techniques. Recent work by Andersen
[And95] proposes a very promising compositional model checking
technique, which has experimentally been shown to improve results obtained
using Binary Decision Diagrams.
In this paper we make Andersen's technique applicable to systems described
by networks of timed automata. We present a quotient construction,
which allows timed automata components to be gradually moved from
the network expression into the specification. The intermediate specifications
are kept small using minimization heuristics suggested by Andersen.
The potential of the combined technique is demonstrated using a prototype
implemented in CAML.
MONA: Monadic Second-Order Logic in Practice
Authors: Henriksen Jesper G. , Jensen Ole J.L. , Jørgensen Michael E. , Klarlund Nils , Paige Robert , Rauhe Theis , Sandholm Anders B.
Published: February 2016

The purpose of this article is to introduce Monadic Second-order
Logic as a practical means of specifying regularity. The logic is a
highly succinct alternative to the use of regular expressions. We have built a tool MONA, which acts as a decision procedure and as a translator to finite-state automata. The tool is based on new algorithms for minimizing finite-state automata that use binary decision diagrams (BDDs) to represent
transition functions in compressed form. A byproduct of this work is a
new bottom-up algorithm to reduce BDDs in linear time without hashing.
The potential applications are numerous. We discuss text processing,
Boolean circuits, and distributed systems. Our main example is an automatic proof of properties for the "Dining Philosophers with Encyclopedia" example by Kurshan and MacMillan. We establish these properties for the parameterized case without the use of induction.
Our results show that, contrary to common beliefs, high computational
complexity may be a desired feature of a specification formalism.
Open Maps (at) Work
Authors: Cheng Allan , Nielsen Mogens
Published: February 2016

The notion of bisimilarity, as defined by Park and Milner,
has turned out to be one of the most fundamental notions of operational
equivalences in the field of process algebras. Not only does it induce
a congruence (largest bisimulation) in CCS which has nice equational
properties, it has also proven itself applicable for numerous models of
parallel computation and settings such as Petri Nets and semantics of
functional languages. In an attempt to understand the relationships and
differences between the extensive amount of research within the field,
Joyal, Nielsen, and Winskel recently presented an abstract category-theoretic
definition of bisimulation. They identify spans of morphisms satisfying certain "path lifting"
 properties, so-called open maps, as a possible abstract definition of bisimilarity.
 In [JNW93] they show, that they can capture Park and Milner's bisimulation.
The aim of this paper is to show that the abstract definition of bisimilarity is applicable
"in practice" by showing how a representative selection of well-known
bisimulations and equivalences, such as e.g. Hennessy's testing equivalence,
Milner and Sangiorgi's barbed bisimulation, and Larsen and Skou's
probabilistic bisimulation, are captured in the setting of open maps and
hence, that the proposed notion of open maps seems successful. Hence,
we confirm that the treatment of strong bisimulation in [JNW93] is not
a one-off application of open maps.
A Complete Equational Axiomatization for MPA with String Iteration
Authors: Aceto Luca , Groote Jan Friso
Published: February 2016

We study equational axiomatizations of bisimulation equivalence for the language obtained by extending Milner's basic CCS with string iteration. String iteration is a variation on the original binary version of the Kleene star operation p*q obtained by restricting the first argument to be a non-empty sequence of atomic actions. We show that, for every positive integer k, bisimulation equivalence over the set of processes in this language with loops of length at most k is finitely axiomatizable. We also offer a countably infinite equational theory that completely axiomatizes bisimulation equivalence over the whole language. We prove that this result cannot be improved upon by showing that no finite equational axiomatization of bisimulation equivalence over basic CCS with string iteration can exist, unless the set of actions is empty.
Type Inference with Selftype
Authors: Palsberg Jens
Published: February 2016

The metavariable self is fundamental in object-oriented languages.
Typing self in the presence of inheritance has been studied by Abadi
and Cardelli, Bruce, and others. A key concept in these developments
is the notion of selftype, which enables flexible type annotations that
are impossible with recursive types and subtyping. Bruce et al. demonstrated
that, for the language TOOPLE, type checking is decidable.
Open until now is the problem of type inference with selftype.
In this paper we present a type inference algorithm for a type
system with selftype, recursive types, and subtyping. The example
language is the object calculus of Abadi and Cardelli, and the type
inference algorithm runs in nondeterministic polynomial time.
Petri Nets and Bisimulations
Authors: Nielsen Mogens , Winskel Glynn
Published: February 2016

Several categorical relationships (adjunctions) between models for concurrency
 have been established, allowing the translation of concepts and
properties from one model to another. A central example is a coreflection
between Petri nets and asynchronous transition systems. The purpose of
the present paper is to illustrate the use of such relationships by transferring
to Petri nets a general concept of bisimulation.
Eta-Expansion Does The Trick
Authors: Danvy Olivier , Malmkjær Karoline , Palsberg Jens
Published: February 2016

Partial-evaluation folklore has it that massaging one's source programs can make them specialize better. In Jones, Gomard, and Sestoft's recent textbook, a whole chapter is dedicated to listing such "binding-time improvements'': non-standard use of continuation-passing style, eta-expansion, and a popular transformation called "The Trick''. We provide a unified view of these binding-time improvements, from a typing perspective.

Just as a proper treatment of product values in partial evaluation requires partially static values, a proper treatment of disjoint sums requires moving static contexts across dynamic case expressions. This requirement precisely accounts for the non-standard use of continuation-passing style encountered in partial evaluation. In this setting, eta-expansion acts as a uniform binding-time coercion between values and contexts, be they of function type, product type, or disjoint-sum type. For the latter case, it achieves "The Trick''.

In this paper, we extend Gomard and Jones's partial evaluator for the lambda-calculus, lambda-Mix, with products and disjoint sums; we point out how eta-expansion for disjoint sums does The Trick; we generalize our earlier work by identifying that eta-expansion can be obtained in the binding-time analysis simply by adding two coercion rules; and we specify and prove the correctness of our extension to lambda-Mix.

 See revised version BRICS-RS-96-17.
The Suffix Tree of a Tree and Minimizing Sequential Transducers
Authors: Breslauer Dany
Published: February 2016

This paper gives a linear-time algorithm for the construction of the
suffix tree of a tree. The suffix tree of a tree is used to obtain an efficient
algorithm for the minimization of sequential transducers.
Solving Equations in the lambda-Calculus using Syntactic Encapsulation
Authors: Goldberg Mayer
Published: February 2016

Syntactic encapsulation is a relation between an expression and one of
its sub-expressions, that constraints how the given sub-expression can
be used throughout the reduction of the expression. In this paper, we
present a class of systems of equations, in which the right-hand side of
each equation is syntactically encapsulated in the left-hand side. This
class is general enough to allow equations to contain self-application,
and to allow unknowns to appear on both sides of the equation. Yet
such a system is simple enough to be solvable, and for a solution
(though of course not its normal form) to be obtainable in constant
time.

Keywords: lambda-calculus, programming calculi.
On Competitive On-Line Paging with Lookahead
Authors: Breslauer Dany
Published: February 2016

This paper studies two methods for improving the competitive efficiency
of on-line paging algorithms: in the first, the on-line algorithm can
use more pages; in the second, it is allowed to have a look-ahead, or in
other words, some partial knowledge of the future. The paper considers a
new measure for the look-ahead size as well as Young's resource-bounded
look-ahead and proves that both measures have the attractive property
that the competitive efficiency of an on-line algorithm with k extra pages
and look-ahead l depends on k+l. Hence, under these measures, an on-line
algorithm has the same benefit from using an extra page or knowing an
extra bit of the future.
A Case Study in Automated Verification Based on Trace Abstractions
Authors: Klarlund Nils , Nielsen Mogens , Sunesen Kim
Published: February 2016

In [14], we proposed a framework for the automatic verification of reactive
systems. Our main tool is a decision procedure, Mona, for Monadic
Second-order Logic (M2L) on finite strings. Mona translates a formula in
M2L into a finite-state automaton. We show in [14] how traces, i.e. finite
executions, and their abstractions can be described behaviorally. These
state-less descriptions can be formulated in terms of customized temporal
logic operators or idioms.
In the present paper, we give a self-contained, introductory account of
our method applied to the RPC-memory specification problem of the 1994
Dagstuhl Seminar on Specification and Refinement of Reactive Systems.
The purely behavioral descriptions that we formulate from the informal
specifications are formulas that may span 10 pages or more.
Such descriptions are a couple of magnitudes larger than usual temporal
logic formulas found in the literature on verification. To securely
write these formulas, we introduce Fido [16] as a reactive system description
language. Fido is designed as a high-level symbolic language for
expressing regular properties about recursive data structures.
All of our descriptions have been verified automatically by Mona from
M2L formulas generated by Fido.
Our work shows that complex behaviors of reactive systems can be
formulated and reasoned about without explicit state-based programming.
With Fido, we can state temporal properties succinctly while enjoying
automated analysis and verification.
Behavioural Equivalence for Infinite Systems—Partially Decidable!
Authors: Nielsen Mogens , Sunesen Kim
Published: February 2016

For finite-state systems non-interleaving equivalences are computationally
at least as hard as interleaving equivalences. In this paper we show
that when moving to infinite-state systems, this situation may change
dramatically.
We compare standard language equivalence for process description languages with two generalizations based on traditional approaches capturing non-interleaving behaviour, pomsets representing global causal dependency, and locality representing spatial distribution of events.
We first study equivalences on Basic Parallel Processes, BPP, a process
calculus equivalent to communication free Petri nets. For this simple
process language our two notions of non-interleaving equivalences agree.
More interestingly, we show that they are decidable, contrasting a result of
Hirshfeld that standard interleaving language equivalence is undecidable.
Our result is inspired by a recent result of Esparza and Kiehn, showing
the same phenomenon in the setting of model checking.
We follow up investigating to which extent the result extends to larger
subsets of CCS and TCSP. We discover a significant difference between
our non-interleaving equivalences. We show that for a certain non-trivial
subclass of processes between BPP and TCSP, not only are the two equivalences different, but one (locality) is decidable whereas the other (pomsets) is not. The decidability result for locality is proved by a reduction to the reachability problem for Petri nets.
Type Inference of Turbo Pascal
Authors: Hougaard Ole I. , Schwartzbach Michael I. , Askari Hosein
Published: February 2016

Type inference is generally thought of as being an exclusive property of
the functional programming paradigm. We argue that such a feature may be
of significant benefit for also standard imperative languages. We present a
working tool (available by WWW) providing these benefits for a full version
of Turbo Pascal. It has the form of a preprocessor that analyzes programs
in which the type annotations are only partial or even absent. The resulting
program has full type annotations, will be accepted by the standard Turbo
Pascal compiler, and has polymorphic use of procedures resolved by means
of code expansion.

Keywords: imperative languages, type inference.
Cut-Elimination for Full Intuitionistic Linear Logic
Authors: Braüner Torben , De Paiva Valeria
Published: February 2016

We describe in full detail a solution to the problem of proving the cut elimination theorem for FILL, a variant of (multiplicative and exponential-free) Linear Logic
introduced by Hyland and de Paiva. Hyland and de Paiva's work used a term assignment
system to describe FILL and barely sketched the proof of cut elimination. In this paper, as well as correcting a small mistake in their paper and extending the
system to deal with exponentials, we introduce a different formal system describing the intuitionistic character of FILL and we provide a full proof of the cut elimination
theorem. The formal system is based on a notion of dependence between formulae within a given proof and seems of independent interest. The procedure for
cut elimination applies to (classical) multiplicative Linear Logic, and we can (with care) restrict our attention to the subsystem FILL. The proof, as usual with cut
elimination proofs, is a little involved and we have not seen it published anywhere.
Open Maps, Behavioural Equivalences, and Congruences
Authors: Cheng Allan , Nielsen Mogens
Published: February 2016

Spans of open maps have been proposed by Joyal, Nielsen,
and Winskel as a way of adjoining an abstract equivalence, P-bisimilarity, to a category of models of computation M, where P is an arbitrary subcategory of observations. Part of the motivation was to recast and generalise Milner's well-known strong bisimulation in this categorical setting.
An issue left open was the congruence properties of P-bisimilarity. We address the following fundamental question: given a category of models of computation M and a category of observations P, are there any conditions under which algebraic constructs viewed as functors preserve P-bisimilarity? We define the notion of functors being P-factorisable,
show how this ensures that P-bisimilarity is a congruence with respect to such functors. Guided by the definition of P-factorisability we show how it is possible to parameterise proofs of functors being P-factorisable
with respect to the category of observations P, i.e., with respect to a behavioural equivalence.

Keywords: Open maps, P-bisimilarity, P-factorisability, congruences, process algebra, category theory.
The Computational Complexity of Some Problems of Linear Algebra
Authors: Buss Jonathan F. , Frandsen Gudmund Skovbjerg , Shallit Jeffery O.
Published: February 2016

We consider the computational complexity of some problems dealing with matrix rank.
 Let E, S be subsets of a commutative ring R.
Let x1, x2, ..., xt be variables. Given a matrix M = M(x1, x2, ..., xt)
with entries chosen from E union {x1, x2, ..., xt}, we want to determine
maxrankS(M) = max rank M(a1, a2, ... , at)
and
minrankS(M) = min rank M(a1, a2, ..., at).
There are also variants of these problems that specify more about the
structure of M, or instead of asking for the minimum or maximum rank,
ask if there is some substitution of the variables that makes the matrix
 invertible or noninvertible.
Depending on E, S, and on which variant is studied, the complexity
of these problems can range from polynomial-time solvable to random
polynomial-time solvable to NP-complete to PSPACE-solvable to
unsolvable.
Optimal Purely Functional Priority Queues
Authors: Brodal Gerth Stølting , Okasaki Chris
Published: February 2016

Brodal recently introduced the first implementation of imperative priority queues to support findMin, insert, and meld in O(1) worst-case time, and deleteMin in O(log n) worst-case time. These bounds are asymptotically optimal among all comparison-based priority queues. In this paper, we adapt
Brodal's data structure to a purely functional setting. In doing so, we both simplify the data structure and clarify its relationship to the binomial queues of Vuillemin, which support all four operations in O(log n) time. Specifically, we derive our implementation from binomial queues in three steps: first, we reduce the running time of insert to O(1) by eliminating the possibility of cascading links; second, we reduce the running time of findMin to O(1) by adding a global root to hold the minimum element; and finally, we reduce the running time of meld to O(1) by allowing priority queues to contain other
priority queues. Each of these steps is expressed using ML-style functors. The last transformation, known as data-structural bootstrapping, is an interesting
application of higher-order functors and recursive structures.
Objects as Mobile Processes
Authors: Hüttel Hans , Kleist Josva
Published: February 2016

The object calculus of Abadi and Cardelli [AC96, AC94b, AC94a]
is intended as model of central aspects of object-oriented programming languages. In this paper we encode the object calculus in the asynchronous pi-calculus without matching and investigate the properties of our encoding.
A Presheaf Semantics of Value-Passing Processes
Authors: Winskel Glynn
Published: February 2016

This paper investigates presheaf models for process calculi with
value passing. Denotational semantics in presheaf models are shown
to correspond to operational semantics in that bisimulation obtained
from open maps is proved to coincide with bisimulation as defined
traditionally from the operational semantics. Both "early" and "late"
semantics are considered, though the more interesting "late" semantics
is emphasised. A presheaf model and denotational semantics is proposed
for a language allowing process passing, though there remains
the problem of relating the notion of bisimulation obtained from open
maps to a more traditional definition from the operational semantics.
A tentative beginning is made of a "domain theory" supporting
presheaf models.
Gödelisation in the lambda-Calculus (Extended Version)
Authors: Goldberg Mayer
Published: February 2016

Gödelisation is a meta-linguistic encoding of terms in a language.
While it is impossible to define an operator in the lambda-calculus which
encodes all closed lambda-expressions, it is possible to construct restricted
versions of such an encoding operator modulo normalisation. In this
paper, we propose such an encoding operator for proper combinators.

Keywords: Programming Calculi; lambda-Calculus; G¨odelisation.
A Compositional Proof of a Real-Time Mutual Exclusion Protocol
Authors: Kristoffersen Kåre J. , Laroussinie Francois , Petersen Kim G. , Pettersson Paul , Yi Wang
Published: February 2016

In this paper, we apply a
compositional proof technique to an automatic
verification of the correctness of
Fischer's mutual exclusion protocol. It
is demonstrated that the technique may
avoid the state-explosion problem. Our
compositional technique has recently been
implemented in a tool, CMC, which gives
experimental evidence that the size of
the verification effort required of the technique
only grows polynomially in the
size of the number of processes in the
protocol. In particular, CMC verifies the
protocol for 50 processes within 172.3
seconds and using only 32MB main memory.
In contrast all existing verification
tools for timed systems will suffer from
the state-explosion problem, and no tool
has to our knowledge succeeded in verifying
the protocol for more than 11 processes.
An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces
Authors: Thiagarajan P. S. , Walukiewicz Igor
Published: February 2016

A basic result concerning LTL, the propositional temporal logic of linear time, is that it is expressively complete; it is equal in expressive power to the first order theory of sequences. We present here a smooth extension of this result to the class of partial orders known as Mazurkiewicz traces. These partial orders arise in a variety of contexts in concurrency theory and they provide the conceptual basis for many of the partial order reduction methods that have been developed in connection with LTL-specifications.

We show that LTrL, our linear time temporal logic, is equal in expressive power to the first order theory of traces when interpreted over (finite and) infinite traces. This result fills a prominent gap in the existing logical theory of infinite traces. LTrL also provides a syntactic characterisation of the so-called trace consistent (robust) LTL-specifications. These are specifications expressed as LTL formulas that do not distinguish between different linearisations of the same trace and hence are amenable to partial order reduction methods.
Lower Bounds for Dynamic Transitive Closure, Planar Point Location, and Parentheses Matching
Authors: Husfeldt Thore , Rauhe Theis , Skyum Søren
Published: February 2016

We give a number of new lower bounds in the cell probe model
with logarithmic cell size, which entails the same bounds on the random access computer with logarithmic word size and unit cost operations. We study the signed prefix sum problem: given a string of length n of zeroes and signed ones, compute the sum of its ith prefix during updates. We show a
lower bound of  Omega(log n/log log n) time per operations, even if the prefix sums are bounded by log n/log log n during all updates. We also show that if the update time is bounded by the product of the worst-case update time and the
answer to the query, then the update time must be Omega(sqrt(log n/ log log n)).
 These results allow us to prove lower bounds for a variety of seemingly unrelated
dynamic problems. We give a lower bound for the dynamic planar point location in monotone subdivisions of
Omega(log n/ log log n) per operation. We give
a lower bound for the dynamic transitive closure problem on upward planar graphs with one source and one sink of
Omega(log n/(log logn)^2) per operation. We give a lower bound of  Omega(sqrt(log n/log log n)) for the dynamic membership problem of any Dyck language with two or more letters. This implies the same
lower bound for the dynamic word problem for the free group with k generators. We also give lower bounds for the dynamic prefix majority and prefix equality problems.
Transition Systems with Independence and Multi-Arcs
Authors: Hildebrandt Thomas Troels , Sassone Vladimiro
Published: February 2016

We extend the model of transition systems with independence in order to provide it with a feature relevant in the noninterleaving analysis of concurrent systems, namely multi-arcs. Moreover, we study the relationships between the category of transition systems with independence and multi-arcs and the category of labeled asynchronous transition systems, extending the results recently obtained by the authors for (simple) transition systems with independence (cf. Proc. CONCUR’96), and yielding a precise characterisation of transition systems with independence and multi-arcs in terms of (event-maximal, diamond-extensional) labelled asynchronous transition systems.
Linear Hashing
Authors: Alon Noga , Dietzfelbinger Martin , Miltersen Peter Bro , Petrank Erez , Tardos Gábor
Published: February 2016

Consider the set H of all linear (or affine) transformations between two vector spaces over a finite field F. We study how good H is as a class of hash functions, namely we consider hashing a set S of size
n into a range having the same cardinality n by a randomly chosen function from H and look at the expected size of the largest hash bucket. H is a universal class of hash functions for any finite field, but
with respect to our measure different fields behave differently.
Compilation and Equivalence of Imperative Objects
Authors: Gordon Andrew D. , Hankin Paul D. , Lassen Søren B.
Published: February 2016

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus and prove them equivalent to the closure-based operational semantics given by Abadi and Cardelli. Our first result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our second result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.

This report is superseded by BRICS-RS-98-55.
Abstract Interpretation in the Operational Semantics Hierarchy
Authors: Schmidt David A.
Published: February 2016

We systematically apply the principles of Cousot-Cousot-style abstract interpretation (a.i.) to the hierarchy of operational semantics definitions - flowchart, big-step, and small-step semantics. For each semantics format we examine the principles of safety and liveness interpretations, first-order and second-order analyses, and termination properties. Application of a.i. to data-flow analysis, model checking, closure analysis, and concurrency theory are demonstrated. Our primary contributions are separating the concerns of safety, termination, and efficiency of representation and showing how a.i. principles apply uniformly to the various levels of the operational semantics hierarchy and their applications.
Span Programs and General Secure Multi-Party Computation
Authors: Cramer Ronald , Damgård Ivan B. , Maurer Ueli
Published: February 2016

The contributions of this paper are three-fold. First, as an abstraction of previously proposed cryptographic protocols we propose two cryptographic primitives: homomorphic
shared commitments and linear secret sharing schemes with an additional multiplication property. We describe new constructions for general secure multi-party computation protocols, both in the cryptographic and the information-theoretic (or secure
channels) setting, based on any realizations of these primitives.
Second, span programs, a model of computation introduced by Karchmer and Wigderson, are used as the basis for constructing new linear secret sharing schemes, from which the two above-mentioned primitives as well as a novel verifiable secret sharing scheme can efficiently be realized. Third, note that linear secret sharing schemes can have arbitrary (as opposed to
threshold) access structures. If used in our construction, this yields multi-party protocols secure against general sets of active adversaries, as long as in the cryptographic (information-theoretic) model no two (no three) of these potentially misbehaving player sets cover the full player set. This is a strict generalization of the threshold-type adversaries and results previously considered in the literature. While this result is new for the cryptographic model, the result for the information-theoretic model was previously proved by Hirt and Maurer. However, in addition to providing an independent proof, our protocols are not recursive and have the potential of being more efficient.
A Relational Account of Call-by-Value Sequentiality
Authors: Riecke Jon G. , Sandholm Anders B.
Published: February 2016

We construct a model for FPC, a purely functional, sequential,
call-by-value language. The model is built from partial continuous
functions, in the style of Plotkin, further constrained to be uniform
with respect to a class of logical relations. We prove that the model
is fully abstract.
CASL for ASF+SDF 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 algebraic
 specification languages, and it is hoped that it may provide
 a focus for future research and development in the use of algebraic
 techniques, as well being attractive for industrial use.
This paper presents Casl for users of the Asf+Sdf framework.
It shows how familiar constructs of Asf+Sdf may be
written in Casl, and considers some problems that may arise
when translating specifications from Asf+Sdf to Casl. It then
explains and motivates various Casl constructs that cannot be
expressed directly in Asf+Sdf. Finally, it discusses the role that
the Asf+Sdf system might play in connection with tool support
for Casl.
Sequential Iteration of Interactive Arguments and an Efficient Zero-Knowledge Argument for NP
Authors: Damgård Ivan B. , Pfitzmann Birgit
Published: February 2016

We study the behavior of interactive arguments under sequential iteration, in particular how this affects the error probability. This problem turns out to be more complex than one might expect from the fact that for interactive proofs, the error trivially decreases exponentially in the number of iterations.
In particular, we study the typical efficient case where the iterated protocol is based on a single instance of a computational problem. This is not a special case of independent
iterations of an entire protocol, and real exponential decrease of the error cannot be expected, but nevertheless, for practical applications, one needs concrete relations
between the complexity and error probability of the underlying problem and that of the iterated protocol. We show how this problem can be formalized and solved using the
theory of proofs of knowledge.
 We also prove that in the non-uniform model of complexity the error probability
of independent iterations of an argument does indeed decrease exponentially - to our knowledge this is the first result about a strictly exponentially small error probability in a computational cryptographic security property.
As an illustration of our first result, we present a very efficient zero-knowledge argument
for circuit satisfiability, and thus for any NP problem, based on any collision-intractable hash function. Our theory applies to show the soundness of this protocol. Using an efficient hash function such as SHA-1, the protocol can handle about 20000 binary gates per second at an error level of 2^−50.

Keywords -- Interactive proofs, arguments, proofs of knowledge, computational security,
efficient general primitives, multi-bit commitment, statistical zero-knowledge.