bluuebunny/crossref_metadata_2025 huggingface dataset:
New-HOPLA--A Higher-Order Process Language with Name Generation
Authors: Winskel Glynn , Nardelli Francesco Zappa
Published: February 2016

This paper introduces new-HOPLA, a concise but powerful language for higher-order nondeterministic processes with name generation. Its origins as a metalanguage for domain theory are sketched but for the most part the paper concentrates on its operational semantics. The language is typed, the type of a process describing the shape of the computation paths it can perform. Its transition semantics, bisimulation, congruence properties and expressive power are explored. Encodings are given of well-known process algebras, including pi-calculus, Higher-Order pi-calculus and Mobile Ambients.
On the Recursive Enumerability of Fixed-Point Combinators
Authors: Goldberg Mayer
Published: February 2016

We show that the set of fixed-point combinators forms a recursively-enumerable subset of a larger set of terms that is (A) not recursively enumerable, and (B) the terms of which are observationally equivalent to fixed-point combinators in any computable context.
A Functional Correspondence between Monadic Evaluators and Abstract Machines for Languages with Computational Effects
Authors: Ager Mads Sig , Danvy Olivier , Midtgaard Jan
Published: February 2016

We extend our correspondence between evaluators and abstract machines from the pure setting of the lambda-calculus to the impure setting of the computational lambda-calculus. We show how to derive new abstract machines from monadic evaluators for the computational lambda-calculus. Starting from (1) a generic evaluator parameterized by a monad and (2) a monad specifying a computational effect, we inline the components of the monad in the generic evaluator to obtain an evaluator written in a style that is specific to this computational effect. We then derive the corresponding abstract machine by closure-converting, CPS-transforming, and defunctionalizing this specific evaluator. We illustrate the construction first with the identity monad, obtaining the CEK machine, and then with a lifting monad, a state monad, and with a lifted state monad, obtaining variants of the CEK machine with error handling, state and a combination of error handling and state.

In addition, we characterize the tail-recursive stack inspection presented by Clements and Felleisen as a lifted state monad. This enables us to combine this stack-inspection monad with other monads and to construct abstract machines for languages with properly tail-recursive stack inspection and other computational effects. The construction scales to other monads--including one more properly dedicated to stack inspection than the lifted state monad--and other monadic evaluators.
An Operational Foundation for Delimited Continuations in the CPS Hierarchy
Authors: Biernacka Malgorzata , Biernacki Dariusz , Danvy Olivier
Published: February 2016

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n, the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.

 We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.
A Quantitative Version of Kirk's Fixed Point Theorem for Asymptotic Contractions
Authors: Gerhardy Philipp
Published: February 2016

In [J.Math.Anal.App.277(2003) 645-650], W.A.Kirk introduced the notion of asymptotic contractions and proved a fixed point theorem for such mappings. Using techniques from proof mining, we develop a variant of the notion of asymptotic contractions and prove a quantitative version of the corresponding fixed point theorem.
Type Checking Semantic Functions in ASDF
Authors: Iversen Jørgen
Published: February 2016

When writing semantic descriptions of programming languages, it is convenient to have tools for checking the descriptions. With frameworks that use inductively defined semantic functions to map programs to their denotations, we would like to check that the semantic functions result in denotations with certain properties. In this paper we present a type system for a modular style of the action semantic framework that, given signatures of all the semantic functions used in a semantic equation defining a semantic function, performs a soft type check on the action in the semantic equation.

We introduce types for actions that describe different properties of the actions, like the type of data they expect and produce, whether they can fail or have side effects, etc. A type system for actions which uses these new action types is presented. Using the new action types in the signatures of semantic functions, the language describer can assert properties of semantic functions and have the assertions checked by an implementation of the type system.

The type system has been implemented for use in connection with the recently developed formalism ASDF. The formalism supports writing language definitions by combining modules that describe single language constructs. This is possible due to the inherent modularity in ASDF. We show how we manage to preserve the modularity and still perform specialised type checks for each module.
Bottom-Up beta-Substitution: Uplinks and lambda-DAGs
Authors: Shivers Olin , Wand Mitchell
Published: February 2016

Terms of the lambda-calculus are one of the most important data structures we have in computer science. Among their uses are representing program terms, advanced type systems, and proofs in theorem provers. Unfortunately, heavy use of this data structure can become intractable in time and space; the typical culprit is the fundamental operation of beta reduction.

If we represent a lambda-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from beta reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement beta reduction in a bottom-up manner, thus avoiding combinatorial explosion in time required to search the term in a top-down fashion.

We present an algorithm for performing beta reduction on lambda terms represented as uplinked DAGs; describe its proof of correctness; discuss its relation to alternate techniques such as Lamping graphs, the suspension lambda-calculus (SLC) and director strings; and present some timings of an implementation.

Besides being both fast and parsimonious of space, the algorithm is particularly suited to applications such as compilers, theorem provers, and type-manipulation systems that may need to examine terms in-between reductions - i.e., the ``readback'' problem for our representation is trivial.

Like Lamping graphs, and unlike director strings or the suspension lambda-calculus, the algorithm functions by side-effecting the term containing the redex; the representation is not a ``persistent'' one.

The algorithm additionally has the charm of being quite simple; a complete implementation of the core data structures and algorithms is 180 lines of fairly straightforward SML.
CPS Transformation of Beta-Redexes
Authors: Danvy Olivier , Nielsen Lasse R.
Published: February 2016

The extra compaction of the most compacting CPS transformation in existence, which is due to Sabry and Felleisen, is generally attributed to (1) making continuations occur first in CPS terms and (2) classifying more redexes as administrative. We show that this extra compaction is actually independent of the relative positions of values and continuations and furthermore that it is solely due to a context-sensitive transformation of beta-redexes. We stage the more compact CPS transformation into a first-order uncurrying phase and a context-insensitive CPS transformation. We also define a context-insensitive CPS transformation that provides the extra compaction. This CPS transformation operates in one pass and is dependently typed.
On the Expressive Power of Extended Process Rewrite Systems
Authors: Kretínský Mojmír , Rehák Vojtech , Strejcek Jan
Published: February 2016

We provide a unified view on three extensions of Process rewrite systems (PRS) and compare their and PRS's expressive power. We show that the class of Petri Nets is less expressible up to bisimulation than the class of Process Algebra extended with finite state control unit. Further we show our main result that the reachability problem for PRS extended with a so called weak finite state unit is decidable.
Zero-Knowledge Proofs and String Commitments Withstanding Quantum Attacks
Authors: Damgård Ivan B. , Fehr Serge , Salvail Louis
Published: February 2016

The concept of zero-knowledge (ZK) has become of fundamental importance in cryptography. However, in a setting where entities are modeled by quantum computers, classical arguments for proving ZK fail to hold since, in the quantum setting, the concept of rewinding is not generally applicable. Moreover, known classical techniques that avoid rewinding have various shortcomings in the quantum setting.

We propose new techniques for building quantum zero-knowledge (QZK) protocols, which remain secure even under (active) quantum attacks. We obtain computational QZK proofs and perfect QZK arguments for any NP language in the common reference string model. This is based on a general method converting an important class of classical honest-verifier ZK (HVZK) proofs into QZK proofs. This leads to quite practical protocols if the underlying HVZK proof is efficient. These are the first proof protocols enjoying these properties, in particular the first to achieve perfect QZK.

As part of our construction, we propose a general framework for building unconditionally hiding (trapdoor) string commitment schemes, secure against quantum attacks, as well as concrete instantiations based on specific (believed to be) hard problems. This is of independent interest, as these are the first unconditionally hiding string commitment schemes withstanding quantum attacks.

Finally, we give a partial answer to the question whether QZK is possible in the plain model. We propose a new notion of QZK, non-oblivious verifier QZK, which is strictly stronger than honest-verifier QZK but weaker than full QZK, and we show that this notion can be achieved by means of efficient (quantum) protocols.
A Simple Proof of a Folklore Theorem about Delimited Control
Authors: Biernacki Dariusz , Danvy Olivier
Published: February 2016

We formalize and prove the folklore theorem that the static delimited-control operators shift and reset can be simulated in terms of the dynamic delimited-control operators control and prompt. The proof is based on a small-step operational semantics that takes the form of an abstract machine.
An Operational Foundation for Delimited Continuations in the CPS Hierarchy
Authors: Biernacka Malgorzata , Biernacki Dariusz , Danvy Olivier
Published: February 2016

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n , the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.

 We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.
A Concrete Framework for Environment Machines
Authors: Biernacka Malgorzata , Danvy Olivier
Published: February 2016

We materialize the common belief that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to Curien's original calculus of closures (an early calculus with explicit substitutions), we extend it minimally so that it can express one-step reduction strategies, and we methodically derive a series of environment machines from the specification of two one-step reduction strategies for the lambda-calculus: normal order and applicative order. The derivation extends Danvy and Nielsen's refocusing-based construction of abstract machines with two new steps: one for coalescing two successive transitions into one, and one for unfolding a closure into a term and an environment in the resulting abstract machine. The resulting environment machines include both the idealized and the original versions of Krivine's machine, Felleisen et al.'s CEK machine, and Leroy's Zinc abstract machine.
On the Dynamic Extent of Delimited Continuations
Authors: Biernacki Dariusz , Danvy Olivier
Published: February 2016

We show that breadth-first traversal exploits the difference between the static delimited-control operator shift (alias S) and the dynamic delimited-control operator control (alias F). For the last 15 years, this difference has been repeatedly mentioned in the literature but it has only been illustrated with one-line toy examples. Breadth-first traversal fills this vacuum.

We also point out where static delimited continuations naturally give rise to the notion of control stack whereas dynamic delimited continuations can be made to account for a notion of 'control queue'.
General Logical Metatheorems for Functional Analysis
Authors: Gerhardy Philipp , Kohlenbach Ulrich
Published: February 2016

In this paper we prove general logical metatheorems which state that for large classes of theorems and proofs in (nonlinear) functional analysis it is possible to extract from the proofs effective bounds which depend only on very sparse local bounds on certain parameters. This means that the bounds are uniform for all parameters meeting these weak local boundedness conditions. The results vastly generalize related theorems due to the second author where the global boundedness of the underlying metric space (resp. a convex subset of a normed space) was assumed. Our results treat general classes of spaces such as metric, hyperbolic, CAT(0), normed, uniformly convex and inner product spaces and classes of functions such as nonexpansive, Hölder-Lipschitz, uniformly continuous, bounded and weakly quasi-nonexpansive ones. We give several applications in the area of metric fixed point theory. In particular, we show that the uniformities observed in a number of recently found effective bounds (by proof theoretic analysis) can be seen as instances of our general logical results.
Measuring the Propagation of Information in Partial Evaluation
Authors: Rohde Henning Korsholm
Published: February 2016

We present the first measurement-based analysis of the information propagated by a partial evaluator. Our analysis is based on measuring implementations of string-matching algorithms, based on the observation that the sequence of character comparisons accurately reflects maintained information. Notably, we can easily prove matchers to be different and we show that they display more variety and finesse than previously believed. As a consequence, we are able to pinpoint differences and inaccuracies in many results previously considered equivalent.

Our analysis includes a framework that lets us obtain string matchers - notably the family of Boyer-Moore algorithms - in a systematic formalism-independent way from a few information-propagation primitives. By leveraging the existing research in string matching, we show that the landscape of information propagation is non-trivial in the sense that small changes in information propagation may dramatically change the properties of the resulting string matchers. We thus expect that this work will prove useful as a test and feedback mechanism for information propagation in the development of advanced program transformations, such as GPC or Supercompilation.
A Calculus for Context-Awareness
Authors: Zimmer Pascal
Published: February 2016

In order to answer the challenge of pervasive computing, we propose a new process calculus, whose aim is to describe dynamic systems composed of agents able to move and react differently depending on their location. This Context-Aware Calculus features a hierarchical structure similar to mobile ambients, and a generic multi-agent synchronization mechanism, inspired from the join-calculus. After general ideas and introduction, we review the full calculus' syntax and semantics, as well as some motivating examples, study its expressiveness, and show how the notion of computation itself can be made context-dependent.
On Counting the Number of Consistent Genotype Assignments for Pedigrees
Authors: Srba Jirí
Published: February 2016

Consistency checking of genotype information in pedigrees plays an important role in genetic analysis and for complex pedigrees the computational complexity is critical. We present here a detailed complexity analysis for the problem of counting the number of complete consistent genotype assignments. Our main result is a polynomial time algorithm for counting the number of complete consistent assignments for non-looping pedigrees. We further classify pedigrees according to a number of natural parameters like the number of generations, the number of children per individual and the cardinality of the set of alleles. We show that even if we assume all these parameters as bounded by reasonably small constants, the counting problem becomes computationally hard (#P-complete) for looping pedigrees. The border line for counting problems computable in polynomial time (i.e. belonging to the class FP) and #P-hard problems is completed by showing that even for general pedigrees with unlimited number of generations and alleles but with at most one child per individual and for pedigrees with at most two generations and two children per individual the counting problem is in FP.
Formal Aspects of Polyvariant Specialization
Authors: Rohde Henning Korsholm
Published: February 2016

We present the first formal correctness proof of an offline polyvariant specialization algorithm for first-order recursive equations. As a corollary, we show that the specialization algorithm generates a program implementing the search phase of the Knuth-Morris- Pratt algorithm from an inefficient but binding-time-improved string matcher.
Faster Algorithms for Computing Longest Common Increasing Subsequences
Authors: Brodal Gerth Stølting , Kaligosi Kanela , Katriel Irit , Kutz Martin
Published: February 2016

We present algorithms for finding a longest common increasing subsequence of two or more input sequences. For two sequences of lengths m and n , where m >= n, we present an algorithm with an output-dependent expected running time of O((m + n l) log log sigma + Sort) and O(m) space, where l is the length of an LCIS, sigma is the size of the alphabet, and 'Sort' is the time to sort each input sequence.

For k >= 3 length-n sequences we present an algorithm running time O(min{k r^2, r log^{k-1} r} + Sort), which improves the previous best bound by more than a factor k for many inputs. In both cases, our algorithms are conceptually quite simple but rely on existing sophisticated data structures.

Finally, we introduce the problem of longest common weakly-increasing (or non-decreasing) subsequences (LCWIS), for which we present an O(m + n log n) time algorithm for the 3-letter alphabet case. For the extensively studied Longest Common Subsequence problem, comparable speedups have not been achieved for small alphabets.
A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations (Preliminary Version)
Authors: Biernacki Dariusz , Danvy Olivier , Millikin Kevin
Published: February 2016

We present a new abstract machine that accounts for dynamic delimited continuations. We prove the correctness of this new abstract machine with respect to a definitional abstract machine. Unlike this definitional abstract machine, the new abstract machine is in defunctionalized form, which makes it possible to state the corresponding higher-order evaluator. This evaluator is in continuation+state passing style, and threads a trail of delimited continuations and a meta-continuation. Since this style accounts for dynamic delimited continuations, we refer to it as `dynamic continuation-passing style.'

 We illustrate that the new machine is more efficient than the definitional one, and we show that the notion of computation induced by the corresponding evaluator takes the form of a monad.
Modular Structural Operational Semantics
Authors: Mosses Peter D.
Published: February 2016

Modular SOS (MSOS) is a variant of conventional Structural Operational Semantics (SOS). Using MSOS, the transition rules for each construct of a programming language can be given incrementally, once and for all, and do not need reformulation when further constructs are added to the language. MSOS thus provides an exceptionally high degree of modularity in language descriptions, removing a shortcoming of the original SOS framework.

After sketching the background and reviewing the main features of SOS, the paper explains the crucial differences between SOS and MSOS, and illustrates how MSOS descriptions are written. It also discusses standard notions of semantic equivalence based on MSOS. An appendix shows how the illustrative MSOS rules given in the paper would be formulated in conventional SOS.
On the Axiomatizability of Priority
Authors: Aceto Luca , Chen Taolue , Fokkink Willem Jan , Ingólfsdóttir Anna
Published: February 2016

This paper studies the equational theory of bisimulation equivalence over the process algebra BCCSP extended with the priority operator of Baeten, Bergstra and Klop. It is proven that, in the presence of an infinite set of actions, bisimulation equivalence has no finite, sound, ground-complete equational axiomatization over that language. This negative result applies even if the syntax is extended with an arbitrary collection of auxiliary operators, and motivates the study of axiomatizations using conditional equations. In the presence of an infinite set of actions, it is shown that, in general, bisimulation equivalence has no finite, sound, ground-complete axiomatization consisting of conditional equations over the language studied in this paper. Finally, sufficient conditions on the priority structure over actions are identified that lead to a finite, ground-complete axiomatization of bisimulation equivalence using conditional equations.
An Interface Theory for Input/Output Automata
Authors: Larsen Kim G. , Nyman Ulrik , Wasowski Andrzej
Published: February 2016

Building on the theory of interface automata by de Alfaro and Henzinger we design an interface language for Lynch's Input/Output Automata, a popular formalism used in the development of distributed asynchronous systems, not addressed by previous interface research. We introduce an explicit separation of assumptions from guarantees not yet seen in other behavioral interface theories. Moreover we derive the composition operator systematically and formally, guaranteeing that the resulting compositions are always the weakest in the sense of assumptions, and the strongest in the sense of guarantees. We also present a method for solving systems of relativized behavioral inequalities as used in our setup and draw a formal correspondence between our work and interface automata. Proofs are provided in an appendix.
Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation
Authors: Srba Jirí
Published: February 2016

We investigate the possibility of (bi)simulation-like preorder/equivalence checking on the class of visibly pushdown automata and its natural subclasses visibly BPA (Basic Process Algebra) and visibly one-counter automata. We describe generic methods for proving complexity upper and lower bounds for a number of studied preorders and equivalences like simulation, completed simulation, ready simulation, 2-nested simulation preorders/equivalences and bisimulation equivalence. Our main results are that all the mentioned equivalences and preorders are EXPTIME-complete on visibly pushdown automata, PSPACE-complete on visibly one-counter automata and P-complete on visibly BPA. Our PSPACE lower bound for visibly one-counter automata improves also the previously known DP-hardness results for ordinary one-counter automata and one-counter nets. Finally, we study regularity checking problems for visibly pushdown automata and show that they can be decided in polynomial time.
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, i/o, stack inspection, proper tail-recursion, and lazy evaluation. Most of the machines already exist but they 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.
On the Equivalence between Small-Step and Big-Step Abstract Machines: A Simple Application of Lightweight Fusion
Authors: Danvy Olivier , Millikin Kevin
Published: February 2016

We show how Ohori and Sasano's recent lightweight fusion by fixed-point promotion provides a simple way to prove the equivalence of the two standard styles of specification of abstract machines: (1) in small-step form, as a state-transition function together with a `driver loop,' i.e., a function implementing the iteration of this transition function; and (2) in big-step form, as a tail-recursive function that directly maps a given configuration to a final state, if any. The equivalence hinges on our observation that for abstract machines, fusing a small-step specification yields a big-step specification. We illustrate this observation here with a recognizer for Dyck words, the CEK machine, and Krivine's machine with call/cc.

The need for such a simple proof is motivated by our current work on small-step abstract machines as obtained by refocusing a function implementing a reduction semantics (a syntactic correspondence), and big-step abstract machines as obtained by CPS-transforming and then defunctionalizing a function implementing a big-step semantics (a functional correspondence).
A Cancellation Theorem for BCCSP
Authors: Aceto Luca , Fokkink Willem Jan , Ingólfsdóttir Anna
Published: February 2016

This paper presents a cancellation theorem for the preorders in van Glabbeek's linear time-branching time spectrum over BCCSP. Apart from having some intrinsic interest, the proven cancellation result plays a crucial role in the study of the cover equations, in the sense of Fokkink and Nain, that characterize the studied semantics. The techniques used in the proof of the cancellation theorem may also have some independent interest.
Ready To Preorder: Get Your BCCSP Axiomatization for Free!
Authors: Aceto Luca , Fokkink Willem Jan , Ingólfsdóttir Anna
Published: February 2016

This paper contributes to the study of the equational theory of the semantics in van Glabbeek's linear time - branching time spectrum over the language BCCSP, a basic process algebra for the description of finite synchronization trees. It offers an algorithm for producing a complete (respectively, ground-complete) equational axiomatization of a behavioral congruence lying between ready simulation equivalence and partial traces equivalence from a complete (respectively, ground-complete) inequational axiomatization of its underlying precongruence--that is, of the precongruence whose kernel is the equivalence. The algorithm preserves finiteness of the axiomatization when the set of actions is finite. It follows that each equivalence in the spectrum whose discriminating power lies in between that of ready simulation and partial traces equivalence is finitely axiomatizable over the language BCCSP if so is its defining preorder.
On the Existence of a Finite Base for Complete Trace Equivalence over BPA with Interrupt
Authors: Aceto Luca , Capobianco Silvio , Ingólfsdóttir Anna
Published: February 2016

We study Basic Process Algebra with interrupt modulo complete trace equivalence. We show that, unlike in the setting of the more demanding bisimilarity, a ground complete finite axiomatization exists. We explicitly give such an axiomatization, and extend it to a finite complete one in the special case when a single action is present.
A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines
Authors: Danvy Olivier , Millikin Kevin
Published: February 2016

We show how Ohori and Sasano's recent lightweight fusion by fixed-point promotion provides a simple way to prove the equivalence of the two standard styles of specification of abstract machines: (1) as a transition function together with a `driver loop' implementing the iteration of this transition function; and (2) as a function directly iterating upon a configuration until reaching a final state, if ever. The equivalence hinges on the fact that the latter style of specification is a fused version of the former one. The need for such a simple proof is motivated by our recent work on syntactic correspondences between reduction semantics and abstract machines, using refocusing.
The SMCL Language Specification
Authors: Nielsen Janus Dam
Published: February 2016

[No abstract available]
Inter-Deriving Semantic Artifacts for Object-Oriented Programming
Authors: Danvy Olivier , Johannsen Jacob
Published: February 2016

We present a new abstract machine for Abadi and Cardelli's untyped calculus of objects. What is special about this semantic artifact (i.e., man-made construct) is that is mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli's monograph. This abstract machine therefore embodies the soundness of Abadi and Cardelli's reduction semantics and natural semantics relative to each other.

To move closer to actual implementations, which use environments rather than actual substitutions, we then represent object methods as closures and in the same inter-derivational spirit, we present three new semantic artifacts: a reduction semantics for a version of Abadi and Cardelli's untyped calculus of objects with explicit substitutions, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and furthermore, they are coherent with the previous ones since as we show, the two abstract machines are bisimilar. Overall, though, the significance of these artifacts lies in them not having been designed from scratch and then proved correct: instead, they were mechanically inter-derived.
Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines
Authors: Danvy Olivier
Published: February 2016

We derive two big-step abstract machines, a natural semantics, and the valuation function of a denotational semantics based on the small-step abstract machine for Core Scheme presented by Clinger at PLDI'98. Starting from a functional implementation of this small-step abstract machine, (1) we fuse its transition function with its driver loop, obtaining the functional implementation of a big-step abstract machine; (2) we adjust this big-step abstract machine so that it is in defunctionalized form, obtaining the functional implementation of a second big-step abstract machine; (3) we refunctionalize this adjusted abstract machine, obtaining the functional implementation of a natural semantics in continuation style; and (4) we closure-unconvert this natural semantics, obtaining a compositional continuation-passing evaluation function which we identify as the functional implementation of a denotational semantics in continuation style. We then compare this valuation function with that of Clinger's original denotational semantics of Scheme.
The Limit View of Infinite Computations
Authors: Klarlund Nils
Published: February 2016

We show how to view computations involving very general liveness properties as limits of finite approximations. This computational model does not require introduction of infinite nondeterminism as with most traditional approaches. Our results allow us directly to relate finite computations in order to infer properties about infinite computations. Thus we are able to provide a mathematical understanding of what simulations and bisimulations are when liveness is involved.

In addition, we establish links between verification theory and classical results in descriptive set theory. Our result on simulations is the essential contents of the Kleene-Suslin Theorem, and our result on bisimulation expresses Martin's Theorem about the determinacy of Borel games.
Automatic Verification of Real-Timed Systems Using EPSILON
Authors: Godskesen Jens Chr. , Larsen Kim G. , Skou Arne
Published: February 2016

In this paper we report on an application and extension of the theory of Timed Modal Specifications (TMS) and its associated verification tool EPSILON. The novel feature with which EPSILON has been extended is the ability to automatically generate  diagnostic information in cases of erroneous refinement steps.
Bootstrapping the Primitive Recursive Functions by 47 Colors
Authors: Riis Søren
Published: February 2016

I construct a concrete coloring of the 3 element subsets of N. It has the property that each homogeneous set {s_0, s_1, s_2, ..., s_r}, r >= s_0 - 1 has its elements spread so much apart that F_{omega}(s_i) < s_{i+1} for i = 1, 2, ..., r -1. It uses only 47 colors. This is more economical than the approximately 160000 colors used by Ketonen and Solovay.
Secure Signature Schemes Based on Interactive Protocols
Authors: Cramer Ronald , Damgård Ivan B.
Published: February 2016

A method is proposed for constructing from interactive protocols digital signature schemes secure against adaptively chosen message attacks. Our main result is that practical secure signature schemes can now also be based on computationally difficult problems other than factoring, such as the discrete logarithm problem.
Linear Logic on Petri Nets
Authors: Engberg Uffe H. , Winskel Glynn
Published: February 2016

This article shows how individual Petri nets form models of Girard's intuitionistic linear logic. It explores questions of expressiveness and completeness of linear logic with respect to this interpretation. An aim is to use Petri nets to give an understanding of linear logic and give some appraisal of the value of linear logic as a specification logic for Petri nets. This article might serve as a tutorial, providing one in-road into Girard's linear logic via Petri nets. With this in mind we have added several exercises and their solutions. We have made no attempt to be exhaustive in our treatment, dedicating our treatment to one semantics of intuitionistic linear logic.

Completeness is shown for several versions of Girard's linear logic with respect to Petri nets as the class of models. The strongest logic considered is intuitionistic linear logic, with (*), --, &, (+) and the exponential ! (``of course''), and forms of quantification. This logic is shown sound and complete with respect to atomic nets (these include nets in which every transition leads to a nonempty multiset of places). The logic is remarkably expressive, enabling descriptions of the kinds of properties one might wish to show of nets; in particular, negative properties, asserting the impossibility of an assertion, can also be expressed. A start is made on decidability issues.
Symmetric Logspace is Closed Under Complement
Authors: Nisan Noam , Ta-Shma Amnon
Published: February 2016

We present a logspace, many-one reduction from the undirected st-connectivity problem to its complement. This shows that SL = co - SL.
Graphs and Decidable Transductions based on Edge Constraints
Authors: Klarlund Nils , Schwartzbach Michael I.
Published: February 2016

We give examples to show that not even  c-edNCE, the most general known notion of context-free graph grammar, is suited for the specification of some common data structures.

To overcome this problem, we use monadic second-order logic and introduce  edge constraints as a new means of specifying a large class of graph families. Our notion stems from a natural dichotomy found in programming practice between ordinary pointers forming spanning trees and auxiliary pointers cutting across.

Our main result is that for certain transformations of graphs definable in monadic second-order logic, the question of whether a graph family given by a specification A is mapped to a family given by a specification B is decidable. Thus a decidable Hoare logic arises.
Efficient String Matching on Coded Texts
Authors: Breslauer Dany
Published: February 2016

The so called "four Russians technique'' is often used to speed up algorithms by encoding several data items in a single memory cell. Given a sequence of n symbols over a constant size alphabet, one can encode the sequence into O(n / lambda) memory cells in O(log(lambda) ) time using n / log(lambda) processors.

This paper presents an efficient CRCW-PRAM string-matching algorithm for coded texts that takes O(log log(m/lambda)) time making only O(n / lambda ) operations, an improvement by a factor of lambda = O(log n) on the number of operations used in previous algorithms. Using this string-matching algorithm one can test if a string is square-free and find all palindromes in a string in O(log log n) time using n / log log n processors.
Automatic Synthesis of Real Time Systems
Authors: Andersen Jørgen H.
Published: February 2016

This paper presents a method for automatically constructing real time systems directly from their specifications. The model-construction problem is considered for implicit specifications of the form:
(A_1 | . . . | A_n | X) sat S
 where S is a real time (logical) specification, A_1, ... , A_n are given (regular) timed agents and the problem is to decide whether there exists (and if possible exhibit) a real time agent X which when put in parallel with A_1, ..., A_n will yield a network satisfying S. The method presented proceeds in two steps: first, the implicit specification of X is transformed into an equivalent direct specification of X; second, a model for this direct specification is constructed (if possible) using a direct model construction algorithm. A prototype implementation of our method has been added to the real time verification tool EPSILON.
Lower Bounds for Monotone Span Programs
Authors: Beimel Amos
Published: February 2016

The model of span programs is a linear algebraic model of computation. Lower bounds for span programs imply lower bounds for contact schemes, symmetric branching programs and for formula size. Monotone span programs correspond also to linear secret-sharing schemes. We present a new technique for proving lower bounds for monotone span programs. The main result proved here yields quadratic lower bounds for the size of monotone span programs, improving on the largest previously known bounds for explicit functions. The bound is asymptotically tight for the function corresponding to a class of 4-cliques.
A Constraint Oriented Proof Methodology based on Modal Transition Systems
Authors: Larsen Kim G.
Published: February 2016

In this paper, we present a constraint-oriented state-based proof methodology for concurrent software systems which exploits compositionality and abstraction for the reduction of the verification problem under investigation. Formal basis for this methodology are Modal Transition Systems allowing loose state-based specifications, which can be refined by successively adding constraints. Key concepts of our method are projective views, separation of proof obligations,  Skolemization and abstraction. The method is even applicable to real time systems
Bisimulation from Open Maps
Authors: Joyal André , Nielsen Mogens , Winskel Glynn
Published: February 2016

An abstract definition of bisimulation is presented. It enables a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets) and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a revision of history-preserving bisimulation of Rabinovitch and Traktenbrot, Goltz and van Glabeek. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has ``refinement'' operators, though further work is required to justify their appropriateness and understand their relation to previous attempts. The general approach yields a logic, generalising Hennessy-Milner logic, which is characteristic for the generalised notion of bisimulation.
Decidability Issues for Petri Nets
Authors: Esparza Javier , Nielsen Mogens
Published: February 2016

This is a survey of some decidability results for Petri nets, covering the last three decades. The presentation is structured around decidability of specific properties, various behavioural  equivalences and finally the model checking problem for temporal logics.
Fast Meldable Priority Queues
Authors: Brodal Gerth Stølting
Published: February 2016

We present priority queues that support the operations MakeQueue,
FindMin, Insert and Meld in worst case time O(1) and Delete and
DeleteMin in worst case time O(log n). They can be implemented on the
pointer machine and require linear space. The time bounds are optimal for
all implementations where Meld takes worst case time o(n).
To our knowledge this is the first priority queue implementation that
supports Meld in worst case constant time and DeleteMin in logarithmic
time.
Inclusion-Exclusion(3) Implies Inclusion-Exclusion(n)
Authors: Dubhashi Devdatt P.
Published: February 2016

We consider a natural generalisation of the familiar inclusion-exclusion formula for sets in the setting of ranked lattices. We show that the generalised inclusion-exclusion formula holds in a lattice if and only if the lattice is distributive and the rank function is modular. As a consequence it turns out (perhaps surprisingly) that the inclusion-exclusion formula for three elements implies the inclusion-exclusion formula for an arbitrary number of elements.
Complexity Results for Model Checking
Authors: Cheng Allan
Published: February 2016

The complexity of model checking branching and linear time
temporal logics over Kripke structures has been addressed in e.g. [SC85,
CES86]. In terms of the size of the Kripke model and the length of the
formula, they show that the model checking problem is solvable in
polynomial time for CTL and NP-complete for L(F). The model checking
problem can be generalised by allowing more succinct descriptions of
systems than Kripke structures. We investigate the complexity of the
model checking problem when the instances of the problem consist of
a formula and a description of a system whose state space is at most
exponentially larger than the description. Based on Turing machines,
we define compact systems as a general formalisation of such system
descriptions. Examples of such compact systems are K-bounded Petri
nets and synchronised automata, and in these cases the well-known
algorithms presented in [SC85, CES86] would require exponential space in
term of the sizes of the system descriptions and the formulas; we present
polynomial space upper bounds for the model checking problem over
compact systems and the logics CTL and L(X,U,S). As an example of
an application of our general results we show that the model checking
problems of both the branching time temporal logic CTL and the linear
time temporal logics L(F) and L(X,U, S) over K-bounded Petri nets are
PSPACE-complete.
Can you Trust your Data?
Authors: Ørbæk Peter
Published: February 2016

A new program analysis is presented, and two compile time methods for this analysis are given. The analysis attempts to answer the question: “Given some trustworthy and some untrustworthy input, can we trust the value of a given variable after execution of some code”. The analyses are based on an abstract interpretation framework and a constraint generation
framework, respectively. The analyses are proved safe with respect to an instrumented semantics. We explicitly deal with a language with pointers and possible aliasing problems.
The constraint based analysis is related directly to the abstract interpretation and therefore indirectly to the instrumented semantics.
Tables should be sorted (on random access machines)
Authors: Fich Faith , Miltersen Peter Bro
Published: February 2016

We consider the problem of storing an n element subset S of a universe
of size m, so that membership queries (is x in S?) can be answered
efficiently. The model of computation is a random access machine with
the standard instruction set (direct and indirect addressing, conditional
branching, addition, subtraction, and multiplication). We show that if s
memory registers are used to store S, where n <= s <= m/n^epsilon, then query
time  Omega(log n) is necessary in the worst case. That is, under these conditions,
the solution consisting of storing S as a sorted table and doing
binary search is optimal. The condition s <= m/n^epsilon is essentially optimal;
we show that if n + m/n^o(1) registers may be used, query time o(log n) is
possible.
A Semantic Theory for Value–Passing Processes Late Approach Part I: A Denotational Model and Its Complete Axiomatization
Authors: Ingólfsdóttir Anna
Published: February 2016

A general class of languages and denotational models for value-passing
calculi based on the late semantic approach is defined. A concrete instantiation
of the general syntax is given. This is a modification of the
standard CCS according to the late approach. A denotational model for
the concrete language is given, an instantiation of the general class. An
equationally based proof system is defined and shown to be sound and
complete with respect to the model.
From Branching to Linear Metric Domains (and back)
Authors: Breugel Franck Van
Published: February 2016

A branching and a linear metric domain - both turned into a category -
are related by means of a reflection and a coreflection.