bluuebunny/crossref_metadata_2025 huggingface dataset:
A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines
Authors: Biernacka Malgorzata , Danvy Olivier
Published: February 2016

We present a systematic construction of environment-based abstract machines from context-sensitive calculi of explicit substitutions, and we illustrate it with ten calculi and machines for applicative order with an abort operation, normal order with generalized reduction and call/cc, the lambda-mu-calculus, delimited continuations, stack inspection, proper tail-recursion, and lazy evaluation. Most of the machines already exist but have been obtained independently and are only indirectly related to the corresponding calculi. All of the calculi are new and they make it possible to directly reason about the execution of the corresponding machines.

In connection with the functional correspondence between evaluation functions and abstract machines initiated by Reynolds, the present syntactic correspondence makes it possible to construct reduction-free normalization functions out of reduction-based ones, which was an open problem in the area of normalization by evaluation.
Distributed Approximation of Fixed-Points in Trust Structures
Authors: Krukow Karl , Twigg Andrew
Published: February 2016

Recently, Carbone, Nielsen and Sassone introduced the trust-structure framework; a semantic model for trust-management in global-scale distributed systems. The framework is based on the notion of trust structures; a set of ``trust-levels'' ordered by two distinct partial orderings. In the model, a unique global trust-state is defined as the least fixed-point of a collection of local policies assigning trust-levels to the entities of the system. However, the framework is a purely denotational model: it gives precise meaning to the global trust-state of a system, but without specifying a way to compute this abstract mathematical object.

 This paper complements q the denotational model of trust structures with operational techniques. It is shown how the least fixed-point can be computed using a simple, totally-asynchronous distributed algorithm. Two efficient protocols for approximating the least fixed-point are provided, enabling sound reasoning about the global trust-state without computing the exact fixed-point. Finally, dynamic algorithms are presented for safe reuse of information between computations, in face of dynamic trust-policy updates.
Exploiting Labels in Structural Operational Semantics
Authors: Mosses Peter D.
Published: February 2016

Structural Operational Semantics (SOS) allows transitions to be labelled. This is fully exploited in SOS descriptions of concurrent systems, but usually not at all in conventional descriptions of sequential programming languages.

This paper shows how the use of labels can provide significantly simpler and more modular descriptions of programming languages. However, the full power of labels is obtained only when the set of labels is made into a category, as in the recently-proposed MSOS variant of SOS.
Reviewing Bounds on the Circuit Size of the Hardest Functions
Authors: Frandsen Gudmund Skovbjerg , Miltersen Peter Bro
Published: February 2016

In this paper we review the known bounds for L(n), the circuit size complexity of the hardest Boolean function on n input bits. The best known bounds appear to be
2^n / n (1 + log n / n - O(1/n)) <= L(n) <= 2^n / n (1 + 3 log n / n + O(1/n)).
 However, the bounds do not seem to be explicitly stated in the literature. We give a simple direct elementary proof of the lower bound valid for the full binary basis, and we give an explicit proof of the upper bound valid for the basis {not, and, or}.
Higher-Order Beta Matching with Solutions in Long Beta-Eta Normal Form
Authors: Støvring Kristian
Published: February 2016

Higher-order matching is a special case of unification of simply-typed lambda-terms: in a matching equation, one of the two sides contains no unification variables. Loader has recently shown that higher-order matching up to beta equivalence is undecidable, but decidability of higher-order matching up to beta-eta equivalence is a long-standing open problem.

We show that higher-order matching up to beta-eta equivalence is decidable if and only if a restricted form of higher-order matching up to beta equivalence is decidable: the restriction is that solutions must be in long beta-eta normal form.
Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
Authors: Delzanno Giorgio , Esparza Javier , Srba Jirí
Published: February 2016

Ping-pong protocols with recursive definitions of agents, but without any active intruder, are a Turing powerful model. We show that under the environment sensitive semantics (i.e. by adding an active intruder capable of storing all exchanged messages including full analysis and synthesis of messages) some verification problems become decidable. In particular we give an algorithm to decide control state reachability, a problem related to security properties like secrecy and authenticity. The proof is via a reduction to a new prefix rewriting model called Monotonic Set-extended Prefix rewriting (MSP). We demonstrate further applicability of the introduced model by encoding a fragment of the ccp (concurrent constraint programming) language into MSP.
A Rational Deconstruction of Landin's J Operator
Authors: Danvy Olivier , Millikin Kevin
Published: February 2016

Landin's J operator was the first control operator for functional languages. It was specified with an extension of the SECD machine, which was the first abstract machine for functional languages. We present a family of compositional evaluation functions corresponding to this extension of the SECD machine, using a series of elementary transformations (transformation into continuation-passing style (CPS) and defunctionalization, chiefly) and their left inverses (transformation into direct style and refunctionalization). To this end, we modernize the SECD machine into a bisimilar one that operates in lock step with the original one but that (1) does not use a data stack and (2) uses the caller-save rather than the callee-save convention for environments. We then characterize the J operator in terms of CPS and in terms of delimited-control operators in the CPS hierarchy. As a byproduct, we also present a reduction semantics for applicative expressions with the J operator, based on Curien's original calculus of explicit substitutions. This reduction semantics mechanically corresponds to the modernized version of the SECD machine and to the best of our knowledge, it provides the first syntactic theory of applicative expressions with the J operator.

The present work is concluded by a motivated wish to see Landin's name added to the list of co-discoverers of continuations. Methodologically, however, it mainly illustrates the value of Reynolds's defunctionalization and of refunctionalization as well as the expressive power of the CPS hierarchy (a) to account for the first control operator and the first abstract machine for functional languages and (b) to connect them to their successors.
Logics for The Applied pi Calculus
Authors: Pedersen Michael David
Published: February 2016

In this master's thesis we present a modal logic for Applied pi which characterises observational equivalence on processes. The motivation is similar to that of Applied pi itself, namely generality: the logic can be adapted to a particular application simply by defining a suitable equational theory on terms.

As a first step towards the logic for Applied pi, a strong version of static equivalence on frames is introduced in which term reductions are observable in addition to equality on terms. We argue that the strong version is meaningful in applications and give two refined definitions based on the notion of cores introduced in work by Boreale et al. for the Spi calculus. The refined definitions are useful because they do not involve universal quantification over arbitrary terms and hence are amenable to a logical characterisation. We show that the refined definitions coincide with the original definition of strong static equivalence under certain general conditions.

A first order logic for frames which characterises strong static equivalence and which yields characteristic formulae is then given based on the refined definitions of strong static equivalence. This logic facilitates direct reasoning about terms in a frame as well as indirect reasoning about knowledge deducible from a frame. The logic for Applied pi is then obtained by adding suitable Hennessy-Milner style modalities to the logic for frames, hence facilitating reasoning about both static and dynamic properties of processes. We finally demonstrate the logic with an application to the analysis of the Needham-Schroeder Public Key Protocol.
A Formal Model for Context-Awareness
Authors: Kjærgaard Mikkel Baun , Bunde-Pedersen Jonathan
Published: February 2016

There is a definite lack of formal support for modeling real- istic context-awareness in pervasive computing applications. The Conawa calculus presented in this paper provides mechanisms for modeling complex and interwoven sets of context-information by extending ambient calculus with new constructs and capabilities. In connection with the calculus we present four scenarios which are used to evaluate Conawa. The calculus is a step in the direction of making formal methods applicable in the area of pervasive computing.
A Finite Equational Base for CCS with Left Merge and Communication Merge
Authors: Aceto Luca , Fokkink Willem Jan , Ingólfsdóttir Anna , Luttik Bas
Published: February 2016

Using the left merge and communication merge from ACP, we present an equational base for the fragment of CCS without restriction and relabelling. Our equational base is finite if the set of actions is finite.
Undecidability Results for Bisimilarity on Prefix Rewrite Systems
Authors: Jancar Petr , Srba Jirí
Published: February 2016

We answer an open question related to bisimilarity checking on labelled transition systems generated by prefix rewrite rules on words. Stirling (1996, 1998) proved the decidability of bisimilarity for normed pushdown processes. This result was substantially extended by Sénizergues (1998, 2005) who showed the decidability for regular (or equational) graphs of finite out-degree (which include unnormed pushdown processes). The question of decidability of bisimilarity for a more general class of so called Type -1 systems (generated by prefix rewrite rules of the form R ---> w where R is a regular language) was left open; this was repeatedly indicated by both Stirling and Sénizergues. Here we answer the question negatively, i.e., we show undecidability of bisimilarity on Type -1 systems, even in the normed case. We complete the picture by considering classes of systems that use rewrite rules of the form w ---> R and R_1 ---> R_2 and show when they yield low undecidability ( Pi^0_1-completeness) and when high undecidability ( Sigma^1_1-completeness), all with and without the assumption of normedness.
HIROIMONO is NP-complete
Authors: Andersson Daniel
Published: February 2016

In a Hiroimono puzzle, one must collect a set of stones from a square grid, moving along grid lines, picking up stones as one encounters them, and changing direction only when one picks up a stone. We show that deciding the solvability of such puzzles is NP-complete.
On Barron and Strachey's Cartesian Product Function
Authors: Danvy Olivier , Spivey Michael
Published: February 2016

Over forty years ago, David Barron and Christopher Strachey published a startlingly elegant program for the Cartesian product of a list of lists, expressing it with a three nested occurrences of the function we now call foldr. This program is remarkable for its time because of its masterful display of higher-order functions and lexical scope, and we put it forward as possibly the first ever functional pearl. We first characterize it as the result of a sequence of program transformations, and then apply similar transformations to a program for the classical power set example. We also show that using a higher-order representation of lists allows a definition of the Cartesian product function where foldr is nested only twice.
A Case for Dynamic Reverse-code Generation
Authors: Lee Jooyong
Published: February 2016

Backtracking (i.e. reverse execution) helps the user of a debugger to naturally think backwards along the execution path of a program, and thinking backwards makes it easy to locate the origin of a bug. So far backtracking has been implemented mostly by state saving or by checkpointing. These implementations, however, inherently do not scale. As has often been said, the ultimate solution for backtracking is to use reverse code: executing the reverse code restores the previous states of a program. In our earlier work, we presented a method to generate reverse code on the fly while running a debugger. This article presents a case study of dynamic reverse-code generation. We compare the memory usage of various backtracking methods in a simple but nontrivial example, a bounded-buffer program. In the case of non-deterministic programs such as this bounded-buffer program, our dynamic reverse-code generation can outperform the existing backtracking methods in terms of memory efficiency.
A Complete, Co-Inductive Syntactic Theory of Sequential Control and State
Authors: Støvring Kristian , Lassen Søren B.
Published: February 2016

We present a new co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references.

We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.

The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence.
Dynamic Normal Forms and Dynamic Characteristic Polynomial
Authors: Frandsen Gudmund Skovbjerg , Sankowski Piotr
Published: February 2016

We present the first fully dynamic algorithm for computing the characteristic polynomial of a matrix. In the generic symmetric case our algorithm supports rank-one updates in O(n^2 log n) randomized time and queries in constant time, whereas in the general case the algorithm works in O(n^2 k log n) randomized time, where k is the number of invariant factors of the matrix. The algorithm is based on the first dynamic algorithm for computing normal forms of a matrix such as the Frobenius normal form or the tridiagonal symmetric form. The algorithm can be extended to solve the matrix eigenproblem with relative error 2^{-b} in additional O(n log^2 n log b) time. Furthermore, it can be used to dynamically maintain the singular value decomposition (SVD) of a generic matrix. Together with the algorithm the hardness of the problem is studied. For the symmetric case we present an Omega(n^2) lower bound for rank-one updates and an Omega(n) lower bound for element updates.
A Study of Syntactic and Semantic Artifacts and its Application to Lambda Definability, Strong Normalization, and Weak Normalization in the Presence of...
Authors: Munk Johan
Published: February 2016

Church's lambda-calculus underlies the syntax (i.e., the form) and the semantics (i.e., the meaning) of functional programs. This thesis is dedicated to studying man-made constructs (i.e., artifacts) in the lambda calculus. For example, one puts the expressive power of the lambda calculus to the test in the area of lambda definability. In this area, we present a course-of-value representation bridging Church numerals and Scott numerals. We then turn to weak and strong normalization using Danvy et al.'s syntactic and functional correspondences. We give a new account of Felleisen and Hieb's syntactic theory of state, and of abstract machines for strong normalization due to Curien, Crégut, Lescanne, and Kluge.
Semantics, Algorithmics and Logic: Basic Research in Computer Science. BRICS Inaugural Talk
Authors: Winskel Glynn
Published: February 2016

This is a transcript of a talk at the inauguration of BRICS, Basic Research in Computer Science, Centre of the Danish Research Foundation, on 2 February 1994 at the Steno museum, University of Aarhus, Denmark.
A Homomorphism Concept for omega-Regularity
Authors: Klarlund Nils
Published: February 2016

The Myhill-Nerode Theorem (that for any regular language, there is a canonical recognizing device) is of paramount importance for the computational handling of many formalisms about finite words.

 For infinite words, no prior concept of homomorphism or structural comparison seems to have generalized the Myhill-Nerode Theorem in the sense that the concept is both language preserving and representable by automata.

In this paper, we propose such a concept based on Families of Right Congruences (Maler and Staiger 93), which we view as a recognizing structures.

We also establish an exponential lower and upper bound on the change in size when a representation is reduced to its canonical form.
Complexity of Nondeterministic Functions
Authors: Andreev Alexander E.
Published: February 2016

The complexity of a nondeterministic function is the minimum possible complexity of its determinisation. The entropy of a nondeterministic function, F, is minus the logarithm of the ratio between the number of determinisations of F and the number of all deterministic functions.

We obtain an upper bound on the complexity of a nondeterministic function with restricted entropy for the worst case.

 These bounds have strong applications in the problem of algorithm derandomization. A lot of randomized algorithms can be converted to deterministic ones if we have an effective hitting set with certain parameters (a set is hitting for a set system if it has a nonempty intersection with any set from the system).

Linial, Luby, Saks and Zuckerman (1993) constructed the best effective hitting set for the system of k-value, n-dimensional rectangles. The set size is polynomial in k log n / epsilon.

Our bounds of nondeterministic functions complexity offer a possibility to construct an effective hitting set for this system with almost linear size in k log n / epsilon.
Count(q) does not imply Count(p)
Authors: Riis Søren
Published: February 2016

I solve a conjecture originally studied by M.Ajtai. It states that for different primes q, p the matching principles Count(q) and Count(p) are logically independent. I prove that this indeed is the case. Actually I show that Count(q) implies Count(p) exactly when each prime in p also is a factor in q.
A Fractal which violates the Axiom of Determinacy
Authors: Riis Søren
Published: February 2016

By use of the axiom of choice I construct a symmetrical and self-similar subset A \subseteq [0,1] \subseteq R. Then by an elementary strategy stealing argument it is shown that A is not determined. The (possible) existence of fractals like A clarifies the status of the controversial Axiom of Determinacy.
Count(q) versus the Pigeon-Hole Principle
Authors: Riis Søren
Published: February 2016

For each p <= 2 there exist a model M* of IDelta_{0}(alpha) which satisfies the Count(p) principle. Furthermore if p contain all prime factors of q there exist n, r in M* and a bijective map f in Set(M*) mapping {1, 2, ..., n} onto {1,2,...,n+q^r}.

A corollary is a complete classification of the Count(q) versus Count(p) problem. Another corollary solves an open question by M. Ajtai.
A Model of Intuitionistic Affine Logic from Stable Domain Theory (Revised and Expanded Version)
Authors: Braüner Torben
Published: February 2016

Girard worked with the category of coherence spaces and continuous stable maps and observed that the functor that forgets the linearity of linear stable maps has a left adjoint. This fundamental observation gave rise to the discovery of Linear Logic. Since then, the category of coherence spaces and linear stable maps, with the comonad induced by the adjunction, has been considered a canonical model of Linear Logic. Now, the same phenomenon is present if we consider the category of pre dI domains and continuous stable maps, and the category of dI domains and linear stable maps; the functor that forgets the linearity has a left adjoint. This gives an alternative model of Intuitionistic Linear Logic. It turns out that this adjunction can be factored in two adjunctions yielding a model of Intuitionistic Affine Logic; the category of pre dI domains and affine stable functions. It is the goal of this paper to show that this category is actually a model of Intuitionistic Affine Logic, and to show that this category moreover has properties which make it possible to use it to model convergence/divergence behaviour and recursion.
Hashing Functions can Simplify Zero-Knowledge Protocol Design (too)
Authors: Damgård Ivan B. , Goldreich Oded , Wigderson Avi
Published: February 2016

In Crypto93, Damgård showed that any constant-round protocol in which the verifier sends only independent, random bits and which is zero-knowledge against the honest verifier can be transformed into a protocol (for the same problem) that is zero-knowledge in general. His transformation was based on the interactive hashing technique of Naor, Ostrovsky, Venkatesan and Yung, and thus the resulting protocol had very large round-complexity.
On Data Structures and Asymmetric Communication Complexity
Authors: Miltersen Peter Bro
Published: February 2016

In this paper we consider two party communication complexity when the input sizes of the two players differ significantly, the ``asymmetric'' case. Most of previous work on communication complexity only considers the total number of bits sent, but we study tradeoffs between the number of bits the first player sends and the number of bits the second sends. These types of questions are closely related to the complexity of static data structure problems in the cell probe model. We derive two generally applicable methods of proving lower bounds, and obtain several applications. These applications include new lower bounds for data structures in the cell probe model. Of particular interest is our ``round elimination'' lemma, which is interesting also for the usual symmetric communication case. This lemma generalizes and abstracts in a very clean form the ``round reduction'' techniques used in many previous lower bound proofs. 
Unified Algebras and Abstract Syntax
Authors: Mosses Peter D.
Published: February 2016

We consider the algebraic specification of abstract syntax in the framework of unified algebras. We illustrate the expressiveness of unified algebraic specifications, and provide a grammar-like notation for specifying abstract syntax, particularly attractive for use in semantic descriptions of full-scale programming languages.
Bisimulations, Games, and Logic
Authors: Nielsen Mogens , Clausen Christian
Published: February 2016

In a recent paper by Joyal, Nielsen, and Winskel, bisimulation is defined in an abstract and uniform way across a wide range of different models for concurrency. In this paper, following a recent trend in theoretical computer science, we characterize their abstract definition game-theoretically and logically in a non-interleaving model. Our characterizations appear as surprisingly simple extensions of corresponding characterizations of interleaving bisimulation.
An Optimal O(log log n) Time Parallel Algorithm for Detecting all Squares in a String
Authors: Apostolico Alberto , Breslauer Dany
Published: February 2016

An optimal O(log log n) time concurrent-read concurrent-write parallel
algorithm for detecting all squares in a string is presented. A tight
lower bound shows that over general alphabets this is the fastest possible
optimal algorithm. When p processors are available the bounds become
Theta(n log n / p + log log 2p). The algorithm uses an optimal parallel
string-matching algorithm together with periodicity properties to locate
the squares within the input string.
From Timed Automata to Logic - and Back
Authors: Laroussinie Francois , Larsen Kim G. , Weise Carsten
Published: February 2016

One of the most successful techniques for automatic verification is that
of model checking. For finite automata there exist since long extremely
efficient model-checking algorithms, and in the last few years these algorithms have been made applicable to the verification of real-time automata using the region-techniques of Alur and Dill.
In this paper, we continue this transfer of existing techniques from the
setting of finite (untimed) automata to that of timed automata. In particular, a timed logic L is put forward, which is sufficiently expressive that we for any timed automaton may construct a single characteristic L formula uniquely characterizing the automaton up to timed bisimilarity. Also, we prove decidability of the satisfiability problem for L with respect to given bounds on the number of clocks and constants of the timed automata to be constructed. None of these results have as yet been succesfully accounted for in the presence of time.
Basic Action Theory
Authors: Lassen Søren B.
Published: February 2016

Action semantics is a semantic description framework with very good
pragmatic properties but until now a rather weak theory for reasoning
about programs. A strong action theory would have a great practical
potential, as it would facilitate reasoning about the large class of
programming languages that can be described in action semantics.
This report develops the foundations for a richer action theory, by
bringing together concepts and techniques from process theory and
from work on operational reasoning about functional programs. Semantic
preorders and equivalences in the action semantics setting are
studied and useful operational techniques for establishing contextual
equivalences are presented. These techniques are applied to establish
equational and inequational action laws and an induction rule.
An n log n Algorithm for Online BDD Refinement
Authors: Klarlund Nils
Published: February 2016

Binary Decision Diagrams are in widespread use in verification systems
for the canonical representation of Boolean functions. A BDD representing
a function phi : B^nu -> N can easily be reduced to its canonical form in
linear time.
In this paper, we consider a natural online BDD refinement problem
and show that it can be solved in O(n log n) if n bounds the size of the
BDD and the total size of update operations.
We argue that BDDs in an algebraic framework should be understood
as minimal fixed points superimposed on maximal fixed points. We propose
a technique of controlled growth of equivalence classes to make the
minimal fixed point calculations be carried out efficiently. Our algorithm
is based on a new understanding of the interplay between the splitting
and growing of classes of nodes.
We apply our algorithm to show that automata with exponentially
large, but implicitly represented alphabets, can be minimized in time
O(n log n), where n is the total number of BDD nodes representing the
automaton.
Trust in the lambda-calculus
Authors: Palsberg Jens , Ørbæk Peter
Published: February 2016

This paper introduces trust analysis for higher-order languages. Trust
analysis encourages the programmer to make explicit the trustworthiness of
data, and in return it can guarantee that no mistakes with respect to trust will
be made at run-time. We present a confluent lambda-calculus with explicit trust
operations, and we equip it with a trust-type system which has the subject
reduction property. Trust information in presented as two annotations of each
function type constructor, and type inference is computable in O(n^3) time.
Type Inference with Nonstructural Subtyping
Authors: Palsberg Jens , Wand Mitchell , O'Keefe Patrick
Published: February 2016

We present an O(n^3) time type inference algorithm for a type
system with a largest type !, a smallest type ?, and the usual ordering
between function types. The algorithm infers type annotations of
minimal size, and it works equally well for recursive types. For the
problem of typability, our algorithm is simpler than the one of Kozen,
Palsberg, and Schwartzbach for type inference without ?. This may
be surprising, especially because the system with ? is strictly more
powerful.
Lower Bounds on Arithmetic Circuits via Partial Derivatives (Preliminary Version)
Authors: Nisan Noam , Wigderson Avi
Published: February 2016

In this paper we describe a new technique for obtaining lower bounds on
restricted classes of non-monotone arithmetic circuits. The heart of this technique is a complexity measure for multivariate polynomials, based on the linear span of their partial derivatives. We use the technique to obtain new lower bounds for computing symmetric polynomials and iterated matrix products.
On the Comparison Complexity of the String Prefix-Matching Problem
Authors: Breslauer Dany , Colussi Livio , Toniolo Laura
Published: February 2016

In this paper we study the exact comparison complexity of the string
prefix-matching problem in the deterministic sequential comparison model
with equality tests. We derive almost tight lower and upper bounds on
the number of symbol comparisons required in the worst case by on-line
prefix-matching algorithms for any fixed pattern and variable text. Unlike
previous results on the comparison complexity of string-matching and
prefix-matching algorithms, our bounds are almost tight for any particular pattern.
We also consider the special case where the pattern and the text are the
same string. This problem, which we call the string self-prefix problem, is
similar to the pattern preprocessing step of the Knuth-Morris-Pratt string-matching
algorithm that is used in several comparison efficient string-matching
and prefix-matching algorithms, including in our new algorithm.
We obtain roughly tight lower and upper bounds on the number of symbol
comparisons required in the worst case by on-line self-prefix algorithms.
Our algorithms can be implemented in linear time and space in the
standard uniform-cost random-access-machine model.
Simple Proofs of Occupancy Tail Bounds
Authors: Dubhashi Devdatt P.
Published: February 2016

We give short proofs of some occupancy tail bounds using the
method of bounded differences in expected form and the notion of
negative association.
A Complete Equational Axiomatization for Prefix Iteration with Silent Steps
Authors: Aceto Luca , Ingólfsdóttir Anna
Published: February 2016

Fokkink ((1994) Inf. Process. Lett. 52: 333{337) has recently proposed a complete
equational axiomatization of strong bisimulation equivalence for MPA_delta^*(A_tau),
i.e., the language obtained by extending Milner's basic CCS with prefix iteration.
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. In this
paper, we extend Fokkink's results to a setting with the unobservable action by
giving a complete equational axiomatization of Milner's observation congruence over
MPA_delta^*(A_tau ).
The axiomatization is obtained by extending Fokkink's axiom system
with two of Milner's standard tau-laws and the following three equations that describe
the interplay between the silent nature of tau and prefix iteration:
tau . x = tau*x
a*(x+tau.y) = a*(x+tau.y + a.y)
tau.(a*x) = a*(tau.a*x) .
Using a technique due to Groote, we also show that the resulting axiomatization is
omega-complete, i.e., complete for equality of open terms.
AMS Subject Classification (1991): 68Q40, 68Q42.
CR Subject Classification (1991): D.3.1, F.3.2, F.4.2.
Keywords and Phrases: Minimal Process Algebra, prefix iteration, equational
logic, omega-completeness, observation congruence.
A Temporal-Logic Approach to Binding-Time Analysis
Authors: Davies Rowan
Published: February 2016

The Curry-Howard isomorphism identifies proofs with typed lambda-
calculus terms, and correspondingly identifies propositions with
types. We show how this isomorphism can be extended to relate
constructive temporal logic with binding-time analysis. In particular,
we show how to extend the Curry-Howard isomorphism
to include the   ("next") operator from linear-time temporal
logic. This yields the simply typed lambda-calculus which we prove
to be equivalent to a multi-level binding-time analysis like those
used in partial evaluation.

Keywords: Curry-Howard isomorphism, partial evaluation, binding-time analysis, temporal logic.
Automated Logical Verification based on Trace Abstractions
Authors: Klarlund Nils , Nielsen Mogens , Sunesen Kim
Published: February 2016

We propose a new and practical framework for integrating the behavioral
reasoning about distributed systems with model-checking methods.
Our proof methods are based on trace abstractions, which relate the
behaviors of the program and the specification. We show that for finite-state
systems such symbolic abstractions can be specified conveniently in
Monadic Second-Order Logic (M2L). Model-checking is then made possible
by the reduction of non-determinism implied by the trace abstraction.
Our method has been applied to a recent verification problem by Broy
and Lamport. We have transcribed their behavioral description of a distributed
program into temporal logic and verified it against another distributed
system without constructing the global program state space. The
reasoning is expressed entirely within M2L and is carried out by a decision
procedure. Thus M2L is a practical vehicle for handling complex temporal
logic specifications, where formulas decided by a push of a button are as
long as 10-15 pages.
Topological Aspects of Traces
Authors: Oosten Jaap Van
Published: February 2016

This paper is a little mathematical study of some models of concurrency. The most elementary one is the concept of an independence structure, which is nothing but a set L with a binary, irreflexive and symmetric relation on it, the independence relation. This leads to the notion of a trace: a string of elements of L, modulo the equivalence generated by swapping adjacent, independent elements of the string.
 There are two aspects of finite traces: they form an order, hence a topology; on the other hand they form a monoid, a quotient of the free monoid on L. Unfortunately, these two points of view are hard to bring together, since the monoid structure can never be continuous or even order-preserving. It is therefore not surprising that many papers on trace theory consist of two, disjoint, parts. In this paper I concentrate on the order-theoretic and topological aspects.
A Complete Deductive System for the mu-Calculus
Authors: Walukiewicz Igor
Published: February 2016

The propositional mu-calculus as introduced by Kozen in [12] is considered.
In that paper a finitary axiomatisation of the logic was presented
but its completeness remained an open question. Here a different finitary
axiomatisation of the logic is proposed and proved to be complete. The
two axiomatisations are compared.
Hardware Verification using Monadic Second-Order Logic
Authors: Basin David A. , Klarlund Nils
Published: February 2016

We show how the second-order monadic theory of strings can be used to specify hardware components and their behavior. This logic admits a decision procedure and counter-model generator based
on canonical automata for formulas. We have used a system implementing these concepts to verify, or find errors in, a number of circuits proposed in the literature. The techniques we use make it easier to
identify regularity in circuits, including those that are parameterized or have parameterized behavioral specifications. Our proofs are semantic and do not require lemmas or induction as would be needed when employing a conventional theory of strings as a recursive data type.

Keywords: Monadic second order logic, automatic theorem proving, hardware verification, mathematical
induction.
A Communication Complexity Proof that Symmetric Functions have Logarithmic Depth
Authors: Brodal Gerth Stølting , Husfeldt Thore
Published: February 2016

We present a direct protocol with logarithmic communication that
finds an element in the symmetric difference of two sets of different size. This
yields a simple proof that symmetric functions have logarithmic circuit depth.
Comparing Transition Systems with Independence and Asynchronous Transition Systems
Authors: Hildebrandt Thomas Troels , Sassone Vladimiro
Published: February 2016

Transition systems with independence and asynchronous transition systems are non-interleaving models for concurrency arising from the same simple idea of decorating transitions with events. They differ for the choice of a derived versus a primitive notion of event which induces considerable differences and makes the two models suitable for different purposes. This opens the problem of investigating their mutual relationships,
to which this paper gives a fully comprehensive answer.
In details, we characterise the category of extensional asynchronous transitions systems as the largest full subcategory of the category of (labelled) asynchronous transition systems which admits TSI, the category of transition systems with independence, as a coreflective subcategory. In addition, we introduce event-maximal asynchronous transitions systems and we show that their category is equivalent to TSI, so providing an exhaustive characterisation of transition systems with independence in terms of asynchronous transition systems.
The Buffer Tree: A New Technique for Optimal I/O Algorithms
Authors: Arge Lars
Published: February 2016

In this paper we develop a technique for transforming an internal-memory tree data structure into an external-memory structure. We show how the technique can be used to develop a search tree like structure, a priority queue, a (one-dimensional) range tree and a segment tree, and give examples of how these structures can be used to develop efficient I/O algorithms. All our algorithms are either extremely simple or straightforward generalizations of known internal-memory algorithms - given the developed external data structures. We believe that algorithms relying on the developed structure will be of practical interest due to relatively small constants in the asymptotic bounds.
On a Question of Arto Salomaa: The Equational Theory of Regular Expressions over a Singleton Alphabet is not Finitely Based
Authors: Aceto Luca , Fokkink Willem Jan , Ingólfsdóttir Anna
Published: February 2016

Salomaa ((1969) Theory of Automata, page 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative answer to this long standing question. The proof of our main result rests upon a model-theoretic argument. For every finite collection of equations, that are sound in the algebra of regular expressions over a singleton alphabet, we build a model in which some valid regular equation fails. The construction of the model mimics the one used by Conway ((1971) Regular Algebra and Finite Machines, page 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions. Our analysis of the model, however, needs to be more refined than the one provided by Conway ibidem.

AMS Subject Classification (1991): 08A70, 03C05, 68Q45, 68Q68,
68Q70.
CR Subject Classification (1991): D.3.1, F.1.1, F.4.1.
Keywords and Phrases: Regular expressions, equational logic, complete axiomatizations.

 
A Machine Verified Distributed Sorting Algorithm
Authors: Andersen Jørgen H. , Harcourt Ed , Prasad K.V.S.
Published: February 2016

We present a verification of a distributed sorting algorithm in ALF,
an implementation of Martin L¨of's type theory. The implementation
is expressed as a program in a prioritized version of CBS, (the Calculus of Broadcasting Systems) which we have implemented in ALF. The specification is expressed in terms of an ALF type which represents the set of all sorted lists and an HML (Hennesey-Milner Logic) formula which expresses that the sorting program will input any number of data until it hears a value triggering the program to begin outputting the data in a sorted fashion. We gain expressive power from the type theory by inheriting the language of data, state expressions, and propositions.
The Fixpoint Bounded-Variable Queries are PSPACE-Complete
Authors: Dziembowski Stefan
Published: February 2016

We study complexity of the evaluation of fixpoint bounded-variable
queries in relational databases. We exhibit a finite database such
that the problem whether a closed fixpoint formula using only 2 individual variables is satisfied in this database is PSPACE-complete. This clarifies the issues raised by Moshe Vardi in [Var95]. We study also the complexity of query evaluation for a number of restrictions of fixpoint logic. In particular we exhibit a sublogic for which the upper bound postulated by Vardi holds.
Statistical Secrecy and Multi-Bit Commitments
Authors: Damgård Ivan B. , Pedersen Torben P. , Pfitzmann Birgit
Published: February 2016

We present and compare definitions of the notion of "statistically
hiding" protocols, and we propose a novel statistically hiding commitment
scheme. Informally, a protocol statistically hides a secret if a
computationally unlimited adversary who conducts the protocol with
the owner of the secret learns almost nothing about it. One definition
is based on the L1-norm distance between probability distributions,
the other on information theory. We prove that the two definitions are
essentially equivalent. For completeness, we also show that statistical
counterparts of definitions of computational secrecy are essentially
equivalent to our main definitions. Commitment schemes are an important
 cryptologic primitive. Their purpose is to commit one party to a certain value,
 while hiding this value from the other party until some later time.
 We present a statistically
hiding commitment scheme allowing commitment to many
bits. The commitment and reveal protocols of this scheme are constant
round, and the size of a commitment is independent of the number of
bits committed to. This also holds for the total communication complexity,
except of course for the bits needed to send the secret when it
is revealed. The proof of the hiding property exploits the equivalence
of the two definitions.

Index terms -- Cryptology, Shannon theory, unconditional security,
statistically hiding, multi-bit commitment, similarity of ensembles
of distributions, zero-knowledge, protocols.

 
Modeling, Sharing, and Recursion for Weak Reduction Strategies using Explicit Substitution
Authors: Benaissa Zine-El-Abidine , Lescanne Pierre , Rose Kristoffer H.
Published: February 2016

We present the lambda sigma^a_w calculus, a formal synthesis of the concepts of
sharing and explicit substitution for weak reduction. We show how
lambda sigma^a_w can be used as a foundation of implementations of functional
programming languages by modelling the essential ingredients of such
implementations, namely weak reduction strategies, recursion, space
leaks, recursive data structures, and parallel evaluation, in a uniform way.
First, we give a precise account of the major reduction strategies
used in functional programming and the consequences of choosing
 lambda-graph-reduction vs. environment-based evaluation. Second, we show
how to add constructors and explicit recursion to give a precise account
of recursive functions and data structures even with respect to
space complexity. Third, we formalize the notion of space leaks in lambda sigma^a_w
and use this to define a space leak free calculus; this suggests optimisations
for call-by-need reduction that prevent space leaking and enables
us to prove that the "trimming" performed by the STG machine does
not leak space.
In summary we give a formal account of several implementation
techniques used by state of the art implementations of functional programming
languages.

Keywords. Implementation of functional programming, lambda
calculus, weak reduction, explicit substitution, sharing, recursion, space
leaks.
Diagnostic Model Checking for Real-Time Systems
Authors: Larsen Kim G. , Pettersson Paul , Yi Wang
Published: February 2016

Uppaal is a new tool suit for automatic verification of networks of
timed automata. In this paper we describe the diagnostic model-checking feature
of Uppaal and illustrates its usefulness through the debugging of (a version
of) the Philips Audio-Control Protocol. Together with a graphical interface of
Uppaal this diagnostic feature allows for a number of errors to be more easily
detected and corrected.
Proof of a Conjecture of S. Mac Lane
Authors: Soloviev Sergei
Published: February 2016

Some sufficient conditions on a Symmetric Monoidal Closed category K are obtained such that a diagram in a free SMC category generated by the set A of atoms commutes if and only if all its interpretations in K are commutative. In particular, the category of vector spaces on any field satisfies these conditions (only this case was considered in the original Mac Lane conjecture). Instead of diagrams, pairs of derivations in Intuitionistic Multiplicative Linear logic can be considered (together with categorical equivalence). Two derivations of the same sequent are equivalent if and only if all their interpretations in K are equal. In fact, the assignment of values (objects of K) to atoms is defined constructively for each pair of derivations. Taking into account a mistake in R. Voreadou's proof of the "abstract coherence theorem" found by the author, it was necessary to modify her description of the class of non-commutative diagrams in SMC categories; our proof of S. Mac Lane conjecture proves also the correctness of the modified description.
Timed Modal Specification —Theory and Tools
Authors: Cerans Karlis , Godskesen Jens Chr. , Larsen Kim G.
Published: February 2016

In this paper we present the theory of Timed Modal Specifications (TMS) together with its implementation, the tool Epsilon. TMS and Epsilon are timed extensions of respectively Modal Specifications [Lar90, LT88] and the Tav system [GLZ89, BLS92].
The theory of TMS is an extension of real-timed process calculi with the specific aim of allowing loose or partial specifications. Looseness of specifications allows implementation details to be left out, thus allowing several and varying implementations. We achieve looseness of specifications by introducing two modalities to transitions of specifications: a may and a must modality. This allows us to define a notion of refinement, generalizing in a natural way the classical notion of bisimulation. Intuitively, the more must-transitions and the fewer may-transitions a specification has, the finer it is. Also, we introduce notions of refinements abstracting from time and/or internal computation.
TMS specifications may be combined with respect to the constructs of the real-time calculus [Wan90]. "Time-sensitive" notions of refinements that are preserved by these constructs are defined,
 thus enabling compositional verification. Epsilon provides automatic tools for verifying refinements. We apply Epsilon to a compositional verification of a train crossing example.
Compositional Safety Logics
Authors: Andersen Jørgen H. , Larsen Kim G.
Published: February 2016

In this paper we present a generalisation of a promising compositional
 model-checking technique introduced for finite-state systems by Andersen
 in [And95] and extended to networks of timed
automata by Larsen et al in [LPY95a, LL95, LPY95b, KLL+97a].
In our generalized setting, programs are modelled as arbitrary
(possibly infinite-state) transition systems and verified with respect
to properties of a basic safety logic. As the fundamental
prerequisite of the compositional technique, it is shown how logical
properties of a parallel program may be transformed into
necessary and sufficient properties of components of the program.
Finally, a set of axiomatic laws are provided useful for
simplifying formulae and complete with respect to validity and
unsatisfiability.