bluuebunny/crossref_metadata_2025 huggingface dataset:
Efficient Inference of Object Types
Authors: Palsberg Jens
Published: February 2016

Abadi and Cardelli have recently investigated a calculus of objects
[2]. The calculus supports a key feature of object-oriented languages:
an object can be emulated by another object that has more refined
methods. Abadi and Cardelli presented four first-order type systems
for the calculus. The simplest one is based on finite types and no
subtyping, and the most powerful one has both recursive types and
subtyping. Open until now is the question of type inference, and
in the presence of subtyping the absence of minimum typings poses
practical problems for type inference [2].
In this paper we give an O(n^3) algorithm for each of the four type
inference problems and we prove that all the problems are P-complete.
We also indicate how to modify the algorithms to handle functions and
records.
Constructing Fixed-Point Combinators Using Application Survival
Authors: Goldberg Mayer
Published: February 2016

The theory of application survival was developed in our Ph.D. thesis
as an approach for reasoning about application in general and self-application
in particular. In this paper, we show how application survival
provides a uniform framework not only for for reasoning about
fixed-points, fixed-point combinators, but also for deriving and comparing
known and new fixed-point combinators.
Non-primitive Recursive Function Definitions
Authors: Agerholm Sten
Published: February 2016

This paper presents an approach to the problem of introducing
non-primitive recursive function definitions in higher order logic. A
recursive specification is translated into a domain theory version, where
the recursive calls are treated as potentially non-terminating. Once we
have proved termination, the original specification can be derived easily.
A collection of algorithms are presented which hide the domain theory
from a user. Hence, the derivation of a domain theory specification
has been automated completely, and for well-founded recursive function
specifications the process of deriving the original specification from the
domain theory one has been automated as well, though a user must
supply a well-founded relation and prove certain termination properties
of the specification. There are constructions for building well-founded
relations easily.
Experiments with ZF Set Theory in HOL and Isabelle
Authors: Agerholm Sten , Gordon Mike
Published: February 2016

Most general purpose proof assistants support versions of
typed higher order logic. Experience has shown that these logics are capable
of representing most of the mathematical models needed in Computer
Science. However, perhaps there exist applications where ZF-style
set theory is more natural, or even necessary. Examples may include
Scott's classical inverse-limit construction of a model of the untyped lambda-calculus
 (D_inf) and the semantics of parts of the Z specification notation.

This paper compares the representation and use of ZF set theory within
both HOL and Isabelle. The main case study is the construction of D_inf.
The advantages and disadvantages of higher-order set theory versus first-order
set theory are explored experimentally. This study also provides a
comparison of the proof infrastructure of HOL and Isabelle.
Gödelisation in the lambda-Calculus
Authors: Goldberg Mayer
Published: February 2016

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

See also BRICS RS-96-5
Petri Nets, Traces, and Local Model Checking
Authors: Cheng Allan
Published: February 2016

It has been observed that the behavioural view of concurrent
systems that all possible sequences of actions are relevant is too generous;
not all sequences should be considered as likely behaviours. Taking
progress fairness assumptions into account one obtains a more realistic
behavioural view of the systems. In this paper we consider the problem
of performing model checking relative to this behavioural view. We
present a CTL-like logic which is interpreted over the model of concurrent
systems labelled 1-safe nets. It turns out that Mazurkiewicz trace
theory provides a natural setting in which the progress fairness assumptions
can be formalized. We provide the first, to our knowledge, set of
sound and complete tableau rules for a CTL-like logic interpreted under
progress fairness assumptions.

keywords: fair progress, labelled 1-safe nets, local model checking, maximal traces, partial orders, inevitability
A Fully Abstract Denotational Model for Observational Congruence
Authors: Ingólfsdóttir Anna , Schalk Andrea
Published: February 2016

A domain theoretical denotational model is given for a simple sublanguage
of CCS extended with divergence operator. The model is derived as
an abstraction on a suitable notion of normal forms for labelled transition
systems. It is shown to be fully abstract with respect to observational
precongruence.
An Adequate Left-Associated Binary Numeral System in the lambda-Calculus
Authors: Goldberg Mayer
Published: February 2016

This paper introduces a sequence of lambda-expressions, modelling the binary
expansion of integers. We derive expressions computing the test
for zero, the successor function, and the predecessor function, thereby
showing the sequence to be an adequate numeral system. These functions
can be computed efficiently. Their complexity is independent of
the order of evaluation.

Keywords: Programming calculi, lambda-calculus, functional programming.
Monadic Second-Order Logic, Graphs and Unfoldings of Transition Systems
Authors: Courcelle Bruno , Walukiewicz Igor
Published: February 2016

We prove that every monadic second-order property of the unfolding
of a transition system is a monadic second-order property of the
system itself. We prove a similar result for certain graph coverings.
Deciding Regularity in Process Algebras
Authors: Kucera Antonin
Published: February 2016

We consider the problem of deciding regularity of normed BPP
and normed BPA processes. A process is regular if it is bisimilar to a
process with finitely many states. We show, that regularity of normed
BPP processes is decidable and we provide a constructive regularity
test. We also show, that the same result can be obtained for the class
of normed BPA processes.
Regularity can be defined also w.r.t. other behavioural equivalences.
We define notions of strong regularity and finite characterisation
and we examine their relationship with notions of regularity
and finite representation. The introduced notion of the finite characterisation
is especially interesting from the point of view of possible
verification of concurrent systems.
In the last section we present some negative results. If we extend
the BPP algebra with the operator of restriction, regularity becomes
undecidable and similar results can be obtained also for other process
algebras.
Axiomatizing Prefix Iteration with Silent Steps
Authors: Aceto Luca , Fokkink Willem Jan , Glabbeek Rob J. van , Ingólfsdóttir Anna
Published: February 2016

Prefix iteration is a variation on the original binary version of the Kleene star operation P*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz. branching congruence, eta-congruence, delay congruence and weak congruence. The completeness proofs for eta-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i.e. terms that may contain process variables. As a by-product, the omega-completeness of the axiomatizations is obtained as well as their completeness for closed terms.

 

AMS Subject Classification (1991): 68Q10, 68Q40, 68Q55.
CR Subject Classification (1991): D.3.1, F.1.2, F.3.2.
Keywords and Phrases: Concurrency, process algebra, basic CCS, prefix iteration, branching bisimulation, eta-bisimulation, delay bisimulation, weak bisimulation, equational logic, complete axiomatizations.
Near-Optimal, Distributed Edge Colouring via the Nibble Method
Authors: Dubhashi Devdatt P. , Grable David A. , Panconesi Alessandro
Published: February 2016

We give a distributed randomized algorithm to edge colour a network. Let G be a graph
with n nodes and maximum degree Delta. Here we prove:
 If Delta = Omega(log^(1+delta) n) for some delta > 0 and lambda > 0 is fixed, the algorithm almost always
colours G with (1 + lambda)Delta colours in time O(log n).
 If s > 0 is fixed, there exists a positive constant k such that if Delta = omega(log^k n), the algorithm almost always colours G with Delta + Delta / log^s n = (1+o(1))Delta colours in time
O(logn + log^s n log log n).
By "almost always" we mean that the algorithm may fail, but the failure probability can be
made arbitrarily close to 0.
The algorithm is based on the nibble method, a probabilistic strategy introduced by
Vojtech R¨odl. The analysis makes use of a powerful large deviation inequality for functions
of independent random variables.
External-Memory Algorithms for Processing Line Segments in Geographic Information Systems
Authors: Arge Lars , Vengroff Darren E. , Vitter Jeffery S.
Published: February 2016

In the design of algorithms for large-scale applications it is essential to consider the problem of minimizing I/O communication. Geographical information systems (GIS) are good examples of such large-scale applications as they frequently handle huge amounts of spatial data. In this paper we develop efficient new external-memory algorithms for a number of important problems involving line segments in the plane, including trapezoid decomposition, batched planar point location, triangulation, red-blue line segment intersection reporting, and general line segment intersection reporting. In GIS systems, the first three problems are useful for rendering and modeling, and the latter two are frequently used for overlaying maps and extracting information
from them.
Semantics-Based Compiling: A Case Study in Type-Directed Partial Evaluation
Authors: Danvy Olivier , Vestergaard René
Published: February 2016

We illustrate a simple and effective solution to semantics-based
compiling. Our solution is based on type-directed partial evaluation, where

- our compiler generator is expressed in a few lines, and is efficient;
 - its input is a well-typed, purely functional definitional interpreter in the manner of denotational semantics;
- the output of the generated compiler is three-address code, in the fashion and efficiency of the Dragon Book;

- the generated compiler processes several hundred lines of source code per second.

The source language considered in this case study is imperative, block-structured,
higher-order, call-by-value, allows subtyping, and obeys
stack discipline. It is bigger than what is usually reported in the literature on semantics-based compiling and partial evaluation.
Our compiling technique uses the first Futamura projection, i.e., we compile programs by specializing a definitional interpreter with respect to this program. Our denitional interpreter is completely straightforward, stack-based, and in direct style. In particular, it requires no clever staging technique (currying, continuations, binding-time improvements, etc.), nor does it rely on any other framework (attribute grammars, annotations, etc.) than the typed lambda-calculus. In particular, it uses no other program analysis than traditional type inference. The overall simplicity and effectiveness of the approach has encouraged us to write this paper, to illustrate this genuine solution to denotational semantics-directed compilation, in the spirit of Scott and Strachey.
Pragmatic Aspects of Type-Directed Partial Evaluation
Authors: Danvy Olivier
Published: February 2016

Type-directed partial evaluation stems from the residualization of static values in dynamic contexts, given their type and the type of their free variables. Its algorithm coincides with the algorithm for coercing
a subtype value into a supertype value, which itself coincides with
Berger and Schwichtenberg's normalization algorithm for the simply typed lambda-calculus. Type-directed partial evaluation thus can be used to specialize a compiled, closed program, given its type.
Since Similix, let-insertion is a cornerstone of partial evaluators for call-by-value procedural languages with computational effects (such as divergence). It prevents the duplication of residual computations, and more generally maintains the order of dynamic side effects in the residual program. This article describes the extension of type-directed partial evaluation
to insert residual let expressions. This extension requires the
user to annotate arrow types with effect information. It is achieved by delimiting and abstracting control, comparably to continuation-based specialization in direct style. It enables type-directed partial evaluation of programs with effects (e.g., a definitional lambda-interpreter for an imperative language) that are in direct style. The residual programs
are in A-normal form. A simple corollary yields CPS (continuation-passing style) terms instead. We illustrate both transformations with two interpreters for Paulson's Tiny language, a classical example in partial evaluation.
Detecting Deadlocks in Concurrent Systems
Authors: Fajstrup Lisbeth , Raussen Martin
Published: February 2016

We use a geometric description for deadlocks occurring in scheduling
problems for concurrent systems to construct a partial order and hence a directed graph, in which the local maxima correspond to deadlocks. Algorithms finding deadlocks are described and assessed.

Keywords: deadlock, partial order, search algorithm, concurrency, distributed
systems.
Thunks and the lambda-Calculus
Authors: Hatcliff John , Danvy Olivier
Published: February 2016

Thirty-five years ago, thunks were used to simulate call-by-name
under call-by-value in Algol 60. Twenty years ago, Plotkin presented continuation-based simulations of call-by-name under call-by-value and vice versa in the lambda-calculus. We connect all three of these classical simulations by factorizing the continuation-based call-by-name simulation Cn with a thunk-based call-by-name simulation T followed by the continuation-based call-by-value simulation Cv extended to thunks.

We show that T actually satisfies all of Plotkin's correctness criteria
for Cn (i.e., his Indifference, Simulation, and Translation
theorems). Furthermore, most of the correctness theorems for Cn can now be seen as simple corollaries of the corresponding theorems for Cv and T.
BDD Algortihms and Cache Misses
Authors: Klarlund Nils , Rauhe Theis
Published: February 2016

Within the last few years, CPU speed has greatly overtaken memory speed. For this reason, implementation of symbolic algorithms - with their extensive use of pointers and hashing - must be reexamined. In this paper, we introduce the concept of cache miss complexity
as an analytical tool for evaluating algorithms depending on pointer chasing. Such algorithms are typical of symbolic computation found in verification. We show how this measure suggests new data structures and algorithms
for multi-terminal BDDs. Our ideas have been implemented in
a BDD package, which is used in a decision procedure for the Monadic Second-order Logic on strings.
Experimental results show that on large examples involving e.g the verification of concurrent programs, our implementation runs 4 to 5 times faster than a widely used BDD implementation.
We believe that the method of cache miss complexity is of general interest to any implementor of symbolic algorithms used in verification.
The Modified Realizability Topos
Authors: Oosten Jaap Van
Published: February 2016

The modified realizability topos is the semantic (and higher order) counterpart of a variant of Kreisel's modified realizability (1957). These years, this realizability has been in the limelight again because of its possibilities for modelling type theory (Streicher, Hyland-Ong-Ritter) and strong normalization.
In this paper this topos is investigated from a general logical and topostheoretic point of view. It is shown that Mod (as we call the topos) is the closed complement of the effective topos inside another one; this turns out to have some logical consequences. Some important subcategories of Mod are described, and a general logical principle is derived, which holds in the larger topos and implies the well-known Independence of Premiss principle.
Fusion Trees can be Implemented with AC0 Instructions only
Authors: Andersson Arne , Miltersen Peter Bro , Thorup Mikkel
Published: February 2016

Addressing a problem of Fredman and Willard, we implement fusion
trees in deterministic linear space using AC0 instructions only.
On the Complexity of Deciding Behavioural Equivalences and Preorders. A Survey
Authors: Hüttel Hans , Shukla Sandeep
Published: February 2016

This paper gives an overview of the computational complexity of all the equivalences in the linear/branching time hierarchy [vG90a] and the preorders
in the corresponding hierarchy of preorders. We consider finite state or regular processes as well as infinite-state BPA [BK84b] processes.
A distinction, which turns out to be important in the finite-state processes, is that of simulation-like equivalences/preorders vs. trace-like equivalences
and preorders. Here we survey various known complexity results for these relations. For regular processes, all simulation-like equivalences and preorders are decidable in polynomial time whereas all trace-like equivalences and preorders are PSPACE-Complete. We also consider interesting special
classes of regular processes such as deterministic, determinate, unary, locally unary, and tree-like processes and survey the known complexity results in
these special cases. For infinite-state processes the results are quite different. For the class of context-free processes or BPA processes any preorder or equivalence beyond bisimulation is undecidable but bisimulation equivalence is polynomial time
decidable for normed BPA processes and is known to be elementarily decidable in the general case. For the class of BPP processes, all preorders and equivalences apart from bisimilarity are undecidable. However, bisimilarity
is decidable in this case and is known to be decidable in polynomial time for normed BPP processes.
The Randomized Complexity of Maintaining the Minimum
Authors: Brodal Gerth Stølting , Chaudhuri Shiva , Radhakrishnan Jaikumar
Published: February 2016

The complexity of maintaining a set under the operations Insert, Delete and FindMin is considered. In the comparison model it is shown that any randomized algorithm with expected amortized cost t comparisons per Insert and Delete has expected cost at least n/(e2^2t) − 1 comparisons for FindMin.
If FindMin is replaced by a weaker operation, FindAny, then it is shown that a randomized algorithm with constant expected cost per operation exists; in contrast, it is shown that no deterministic algorithm can have constant cost
per operation. Finally, a deterministic algorithm with constant amortized cost per operation for an offline version of the problem is given.
The Complexity of Computing the k-ary Composition of a Binary Associative Operator
Authors: Brodal Gerth Stølting , Skyum Sven
Published: February 2016

We show that the problem of computing all contiguous k-ary compositions of a sequence of n values under an associative and commutative operator requires 3(k−1)/ (k+1)n − O(k) operations.
For the operator max we show in contrast that in the decision
tree model the complexity is (1+ Theta(1/sqrt(k)) n − O(k).

Finally we show that the complexity of the corresponding on-line problem for the operator max is (2 − 1/(k−1)) n − O(k).
Weak Semantics Based on Lighted Button Pressing Experiments. An Alternative Characterization of the Readiness Semantics
Authors: Ingólfsdóttir Anna
Published: February 2016

Imposing certain restrictions on the transition system that defines the behaviour of a process allows us to characterize the readiness semantics of [OH86] by means of black-box testing experiments, or more precisely by lighted button testing experiments [BM92]. As divergence is considered we give the semantics as a preorder, the readiness preorder, which kernel coincides with the readiness equivalence of [OH86]. This leads to a bisimulation like characterization and a modal characterization of the semantics. A concrete language, recursive free CCS without tau, is introduced, a proof system defined and it is shown to be sound and complete with respect to the readiness preorder. In the completeness proof the modal characterization plays an important role as it allows us to prove algebraicity of the preorder purely operationally.
A Decision Algorithm for Linear Isomorphism of Types with Complexity Cn(log2(n))
Authors: Andreev Alexander E. , Soloviev Sergei
Published: February 2016

It is known that ordinary isomorphisms (associativity and commutativity
of "times", isomorphisms for "times" unit and currying)
provide a complete axiomatisation for linear isomorphism of types.
One of the reasons to consider linear isomorphism of types instead of
ordinary isomorphism was that better complexity could be expected.
Meanwhile, no upper bounds reasonably close to linear were obtained.
We describe an algorithm deciding if two types are linearly isomorphic
with complexity Cn(log2(n)).
Meaningful and Meaningless Solutions for Cooperative N-person Games
Authors: Pekec Aleksandar
Published: February 2016

Game values often represent data that can be measured in more
than one acceptable way (e.g. monetary amounts). We point out that
in such a case a statement about cooperative n-person game model
might be "meaningless" in the sense that its truth or falsity depends on
the choice of an acceptable way to measure game values. In particular
we analyze statements about solution concepts such as the core, stable
sets, the nucleolus, the Shapley value (and its generalizations).

Keywords: Cooperative n-person Games, Measurement, Sensitivity
Analysis.
Scalings in Linear Programming: Necessary and Sufficient Conditions for Invariance
Authors: Pekec Aleksandar
Published: February 2016

We analyze invariance of the conclusion of optimality for the linear
programming problem under scalings (linear, affine, . . . ) of various
problem parameters such as: the coefficients of the objective function,
the coefficients of the constraint vector, the coefficients of one or more
rows (columns) of the constraint matrix. Measurement theory concepts
play a central role in our presentation and we explain why such
approach is a natural one.

Keywords: Sensitivity Analysis, Scaling, Measurement
Hypergraph Optimization Problems: Why is the Objective Function Linear?
Authors: Pekec Aleksandar
Published: February 2016

Choosing an objective function for an optimization problem is a
modeling issue and there is no a-priori reason that the objective function
must be linear. Still, it seems that linear 0-1 programming formulations
are overwhelmingly used as models for optimization problems
over discrete structures. We show that this is not an accident. Under
some reasonable conditions (from the modeling point of view), the
linear objective function is the only possible one.
Rn and Gn Logics
Authors: Hintermeier Claus , Kirchner Hélene , Mosses Peter D.
Published: February 2016

This paper proposes a simple, set-theoretic framework providing
expressive typing, higher-order functions and initial models at
the same time. Building upon Russell's ramified theory of types, we develop
the theory of Rn-logics, which are axiomatisable by an order-sorted
equational Horn logic with a membership predicate, and of Gn-logics,
that provide in addition partial functions. The latter are therefore more
adapted to the use in the program specification domain, while sharing
 interesting properties, like existence of an initial model, with Rn-logics.
 Operational semantics of Rn-/Gn-logics presentations is obtained through
order-sorted conditional rewriting.
Combining Algebraic and Set-Theoretic Specifications (Extended Version)
Authors: Hintermeier Claus , Kirchner Hélene , Mosses Peter D.
Published: February 2016

Specification frameworks such as B and Z provide power sets and cartesian
products as built-in type constructors, and employ a rich notation for
defining (among other things) abstract data types using formulae of predicate
logic and lambda-notation. In contrast, the so-called algebraic specification
frameworks often limit the type structure to sort constants and
first-order functionalities, and restrict formulae to (conditional) equations.
Here, we propose an intermediate framework where algebraic specifications
are enriched with a set-theoretic type structure, but formulae remain in the
logic of equational Horn clauses. This combines an expressive yet modest
specification notation with simple semantics and tractable proof theory.
Pushdown Processes: Games and Model Checking
Authors: Walukiewicz Igor
Published: February 2016

Games given by transition graphs of pushdown processes are considered.
It is shown that if there is a winning strategy in such a
game then there is a winning strategy that is realized by a pushdown
process. This fact turns out to be connected with the model checking
problem for the pushdown automata and the propositional mu-calculus.
It is shown that this model checking problem is DEXPTIME-complete.
An Adequate Left-Associated Binary Numeral System in the lambda-Calculus (Revised Version)
Authors: Goldberg Mayer
Published: February 2016

This paper introduces a sequence of lambda-expressions modelling the binary expansion of integers. We derive expressions computing the test for zero, the successor function, and the predecessor function, thereby showing the sequence to be an adequate numeral system. These functions can be computed efficiently. Their complexity is independent of the order of evaluation.

Keywords: Programming calculi, lambda-calculus, functional programming.
UPPAAL in 1995
Authors: Bengtsson Johan , Larsen Kim G. , Larsson Fredrik , Pettersson Paul , Yi Wang
Published: February 2016

UPPAAL is a tool suite for automatic verification of safety and
bounded liveness properties of real-time systems modeled as networks of timed automata
[12, 9, 4], developed during the past two years. In this paper, we summarize
the main features of UPPAAL in particular its various extensions developed in 1995
as well as applications to various case-studies, review and provide pointers to the
theoretical foundation.
Linear Zero-Knowledgde. A Note on Efficient Zero-Knowledge Proofs and Arguments
Authors: Damgård Ivan B. , Cramer Ronald
Published: February 2016

We present a zero-knowledge proof system [19] for any NP language L, which
allows showing that x in L with error probability less than 2^−k using communication
corresponding to O(|x|^c) + k bit commitments, where c is a constant depending only
on L. The proof can be based on any bit commitment scheme with a particular set
of properties. We suggest an efficient implementation based on factoring.
We also present a 4-move perfect zero-knowledge interactive argument for any NP-language
L. On input x in L, the communication complexity is O(|x|^c) max(k; l)
bits, where l is the security parameter for the prover. Again, the protocol can be
based on any bit commitment scheme with a particular set of properties. We suggest
efficient implementations based on discrete logarithms or factoring.
We present an application of our techniques to multiparty computations, allowing
for example t committed oblivious transfers with error probability 2^−k to be done
simultaneously using O(t+k) commitments. Results for general computations follow
from this.
As a function of the security parameters, our protocols have the smallest known
asymptotic communication complexity among general proofs or arguments for NP.
Moreover, the constants involved are small enough for the protocols to be practical in
a realistic situation: both protocols are based on a Boolean formula Phi containing and-
, or- and not-operators which verifies an NP-witness of membership in L. Let n be
the number of times this formula reads an input variable. Then the communication
complexity of the protocols when using our concrete commitment schemes can be
more precisely stated as at most 4n + k + 1 commitments for the interactive proof
and at most 5nl +5l bits for the argument (assuming k <= l). Thus, if we use k = n,
the number of commitments required for the proof is linear in n.
Both protocols are also proofs of knowledge of an NP-witness of membership in
the language involved.
Bisimulations for Asynchronous Mobile Processes
Authors: Hansen Martin , Hüttel Hans , Kleist Josva
Published: February 2016

Within the past few years there has been renewed interest in the
study of value-passing process calculi as a consequence of the emergence of the pi-calculus. Here, [MPW89] have determined two variants of the notion of bisimulation, late and early bisimilarity. Most recently [San93] has proposed the new notion of open bisimulation equivalence.
In this paper we consider Plain LAL, a mobile process calculus which differs from the pi-calculus in the sense that the communication of data values happens asynchronously. The surprising result is that in the presence of asynchrony, the open, late and early bisimulation equivalences coincide - this in contrast to the pi-calculus where they are distinct. The result allows us to formulate a common equational theory which is sound and complete for finite terms of Plain LAL.
Dictionaries on AC^0 RAMs: Query Time Theta(√log n/log log n) is Necessary and Sufficient
Authors: Andersson Arne , Miltersen Peter Bro , Riis Søren , Thorup Mikkel
Published: February 2016

[No abstract available for preview]
Bistructures, Bidomains and Linear Logic
Authors: Curien Pierre-Louis , Plotkin Gordon , Winskel Glynn
Published: February 2016

Bistructures are a generalisation of event structures which allow
a representation of spaces of functions at higher types in an orderextensional setting. The partial order of causal dependency is replaced by two orders, one associated with input and the other with output in the behaviour of functions. Bistructures form a categorical model of Girard's classical linear logic in which the involution of linear logic is modelled, roughly speaking, by a reversal of the roles of input and output. The comonad of the model has an associated co-Kleisli category which is closely related to that of Berry's bidomains (both have equivalent non-trivial full sub-cartesian closed categories).
How to Believe a Machine-Checked Proof
Authors: Pollack Robert
Published: February 2016

Suppose I say "Here is a machine-checked proof of Fermat's last theorem (FLT)". How can you use my putative machine-checked proof as evidence for belief in
FLT? I start from the position that you must have some personal experience of understanding to attain belief, and to have this experience you must engage your intuition and other mental processes which are impossible to formalise. By machine-checked proof I mean a formal derivation in some given formal
system; I am talking about derivability, not about truth. Further, I want to talk about actually believing an actual formal proof, not about formal proofs in principle; to be interesting, any approach to this problem must be feasible. You might try to read my proof, just as you would a proof in a journal; however,
with the current state of the art, this proof will surely be too long for you to have confidence that you have understood it. This paper presents a technological
approach for reducing the problem of believing a formal proof to the same psychological and philosophical issues as believing a conventional proof in a mathematics journal. The approach is not entirely successful philosophically as there seems to be a fundamental difference between machine checked mathematics,
which depends on empirical knowledge about the physical world, and informal mathematics, which needs no such knowledge (see section 3.2.2).
In the rest of this introduction I outline the approach and mention related work. In following sections I discuss what we expect from a proof, add details to the approach, pointing out problems that arise, and concentrate on what I believe
is the primary technical problem: expressiveness and feasibility for checking of formal systems and representations of mathematical notions.
Classifying Toposes for First Order Theories
Authors: Butz Carsten , Johnstone Peter T.
Published: February 2016

By a classifying topos for a first-order theory T, we mean a topos
E such that, for any topos F, models of T in F correspond exactly to
open geometric morphisms F ! E. We show that not every (infinitary)
first-order theory has a classifying topos in this sense, but we
characterize those which do by an appropriate `smallness condition',
and we show that every Grothendieck topos arises as the classifying
topos of such a theory. We also show that every first-order theory
 has a conservative extension to one which possesses
 a classifying topos, and we obtain a Heyting-valued completeness
 theorem for infinitary first-order logic.
Searching Constant Width Mazes Captures the AC0 Hierarchy
Authors: Barrington David A. Mix , Lu Chi-Jen , Miltersen Peter Bro , Skyum Sven
Published: February 2016

We show that searching a width k maze is complete for Pi_k, i.e.,
for the k'th level of the AC0 hierarchy. Equivalently, st-connectivity
for width k grid graphs is complete for Pi_k. As an application, we
show that there is a data structure solving dynamic st-connectivity for
 constant width grid graphs with time bound O(log log n) per operation
 on a random access machine. The dynamic algorithm is derived from
 the parallel one in an indirect way using algebraic tools.
A Definability Theorem for First Order Logic
Authors: Butz Carsten , Moerdijk Ieke
Published: February 2016

In this paper, we will present a definability theorem for first order logic.
This theorem is very easy to state, and its proof only uses elementary tools. To explain the theorem, let us first observe that if M is a model of a theory T in a language L, then, clearly, any definable subset S M (i.e., a subset S = {a | M |= phi(a)} defined by some formula phi) is invariant under all
automorphisms of M. The same is of course true for subsets of M" defined
by formulas with n free variables.
 Our theorem states that, if one allows Boolean valued models, the converse holds. More precisely, for any theory T we will construct a Boolean valued model M, in which precisely the T-provable formulas hold, and in which every (Boolean valued) subset which is invariant under all automorphisms of M is definable by a formula of L.
Our presentation is entirely selfcontained, and only requires familiarity
with the most elementary properties of model theory. In particular, we have added a first section in which we review the basic definitions concerning
Boolean valued models.
The Boolean algebra used in the construction of the model will be presented concretely as the algebra of closed and open subsets of a topological space X naturally associated with the theory T. The construction of this space is closely related to the one in [1]. In fact, one of the results in that paper could be interpreted as a definability theorem for infinitary logic, using topological rather than Boolean valued models.
Proof Theory and Computational Analysis
Authors: Kohlenbach Ulrich
Published: February 2016

In this survey paper we start with a discussion how functionals of finite type can be used for the proof-theoretic extraction of numerical data (e.g. effective
uniform bounds and rates of convergence) from non-constructive proofs in numerical analysis. We focus on the case where the extractability of polynomial bounds is guaranteed.
This leads to the concept of hereditarily polynomial bounded analysis (PBA). We indicate the mathematical range of PBA which turns out to be surprisingly large. Finally we discuss the relationship between PBA and so-called feasible analysis
FA. It turns out that both frameworks are incomparable. We argue in favor of the thesis that PBA offers the more useful approach for the purpose of extracting mathematically interesting bounds from proofs. In a sequel of appendices to this paper we indicate the expressive power of PBA.
Presheaf Models for the pi-Calculus
Authors: Cattani Gian Luca , Stark Ian , Winskel Glynn
Published: February 2016

Recent work has shown that presheaf categories provide a general model of concurrency, with an inbuilt notion of bisimulation based on open maps. Here it is shown how this approach can also handle systems where the language of actions may change dynamically as a process evolves. The example is the pi-calculus, a calculus for `mobile processes' whose communication topology varies as channels are created and discarded. A denotational semantics is described for the pi-calculus within an indexed category of profunctors; the model is fully abstract for bisimilarity, in the sense that bisimulation in the model, obtained from open maps, coincides with the usual bisimulation obtained from the operational semantics of the pi-calculus. While attention is concentrated on the `late' semantics of the pi-calculus, it is indicated how the `early' and other variants can also be captured.

 

A version of this paper appears in Category Theory and Computer Science: Proceedings of the 7th International Conference CTCS '97, Lecture Notes in Computer Science 1290. Springer-Verlag, September 1997.
Names, Equations, Relations: Practical Ways to Reason about new
Authors: Stark Ian
Published: February 2016

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state
in the form of dynamically-generated names. These names can be created locally, passed around, and compared with one another. Through the interaction between
names and functions, the language can capture notions of scope, visibility and sharing. Originally motivated by the study of references in Standard ML, the nu-calculus
has connections to local declarations in general; to the mobile processes of the pi-calculus; and to security protocols in the spi-calculus.
 This paper introduces a logic of equations and relations which allows one to
reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of
contextual equivalence (also known as observational, or observable, equivalence). The logic is based on earlier operational techniques, providing the same power but
in a much more accessible form. In particular it allows intuitive and direct proofs of all contextual equivalences between first-order functions with local names.

This supersedes the earlier BRICS Report RS-96-31. It also expands on the paper presented in Typed Lambda Calculi and Applications: Proceedings of the Third
International Conference TLCA '97, Lecture Notes in Computer Science 1210, Springer-Verlag 1997.
Bisimulation for Labelled Markov Processes
Authors: Blute Richard , Desharnais Josée , Edalat Abbas , Panangaden Prakash
Published: February 2016

In this paper we introduce a new class of labelled transition systems
- Labelled Markov Processes - and define bisimulation for them.
Labelled Markov processes are probabilistic labelled transition systems
where the state space is not necessarily discrete, it could be the
reals, for example. We assume that it is a Polish space (the underlying
topological space for a complete separable metric space). The mathematical
 theory of such systems is completely new from the point of
view of the extant literature on probabilistic process algebra; of course,
it uses classical ideas from measure theory and Markov process theory.
The notion of bisimulation builds on the ideas of Larsen and Skou and
of Joyal, Nielsen and Winskel. The main result that we prove is that
a notion of bisimulation for Markov processes on Polish spaces, which
extends the Larsen-Skou denition for discrete systems, is indeed an
equivalence relation. This turns out to be a rather hard mathematical
result which, as far as we know, embodies a new result in pure probability
theory. This work heavily uses continuous mathematics which
is becoming an important part of work on hybrid systems.
Quantum Entanglement and Communication Complexity
Authors: Buhrman Harry , Cleve Richard , Dam Wim Van
Published: February 2016

We consider a variation of the multi-party communication complexity scenario where the parties are supplied with an extra resource: particles
in an entangled quantum state. We show that, although a prior
quantum entanglement cannot be used to simulate a communication channel, it can reduce the communication complexity of functions in
some cases. Specifically, we show that, for a particular function among three parties (each of which possesses part of the function's input), a prior quantum entanglement enables them to learn the value of the
function with only three bits of communication occurring among the parties, whereas, without quantum entanglement, four bits of communication are necessary. We also show that, for a particular two-party probabilistic communication complexity problem, quantum entanglement
results in less communication than is required with only classical
random correlations (instead of quantum entanglement). These results are a noteworthy contrast to the well-known fact that quantum entanglement cannot be used to actually simulate communication among
remote parties.
What Is a ‘Good’ Encoding of Guarded Choice?
Authors: Nestmann Uwe
Published: February 2016

The pi-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the pi-calculus with asynchronous output and no choice. As a corollary, Palamidessi recently proved that there is no fully compositional encoding
from the former into the latter that preserves divergence-freedom and symmetries. This paper shows that there are nevertheless `good' encodings between these calculi.
In detail, we present a series of encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice, and investigate them with respect to compositionality and divergence-freedom. The first
and second encoding satisfy all of the above criteria, but various `good' candidates for the third encoding - inspired by an existing distributed implementation - invalidate one or the other criterion. While essentially confirming Palamidessi's result, our study
suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes.
Some Lambda Calculus and Type Theory Formalized
Authors: McKinna James , Pollack Robert
Published: February 2016

"This paper is about our hobby." That is the first sentence of [MP93], the first report on our formal development of lambda calculus and type theory, written in autumn 1992. We have continued to pursue this hobby on and off ever since, and have developed a substantial body of formal knowledge, including Church-Rosser and standardization
theorems for beta reduction, and the basic theory of
Pure Type Systems (PTS) leading to the strengthening theorem and type checking algorithms for PTS. Some of this work is reported in [MP93, vBJMP94, Pol94b, Pol95]. In the present paper we survey this work, including some new proofs, and point out what we feel has been learned about the general issues of formalizing mathematics. On the technical side, we describe an abstract, and simplified, proof of standardization for beta reduction, not previously published, that does
not mention redex positions or residuals. On the general issues, we emphasize the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts. The LEGO Proof Development System [LP92] was used to check the work in an implementation of the Extended Calculus of Constructions
(ECC) with inductive types [Luo94]. LEGO is a refinement style
proof checker, publicly available by ftp and WWW, with a User's Manual [LP92] and a large collection of examples. Section 1.3 contains information on accessing the formal development described in this paper. Other interesting examples formalized in LEGO include program specification and data refinement [Luo91], strong normalization of System F [Alt93], synthetic domain theory [Reu95, Reu96], and operational semantics for imperative programs [Sch97].
On the Finitary Characterization of pi-Congruences
Authors: Quaglia Paola
Published: February 2016

Some alternative characterizations of late full congruences, either strong or weak, are presented. Those congruences are classically defined by requiring the corresponding ground bisimilarity under all name substitutions.
We first improve on those infinitary definitions by showing that congruences can be alternatively characterized in the pi-calculus by sticking to a finite
number of carefully identified substitutions, and hence, by resorting to only a finite number of ground bisimilarity checks.
Then we investigate the same issue in both the ground and the non-ground pi-xsi-calculus, a CCS-like process algebra whose ground version has already been proved to coincide with ground pi-calculus. The pi-xsi-calculus perspective allows processes to be explicitly interpreted as functions of their free names. As a
result, a couple of alternative characterizations of pi-congruences are given, each of them in terms of the bisimilarity of one single pair of pi-xsi-processes. In one case, we exploit lambda-closures of processes, so inducing the effective generation
of the substitutions necessary to infer non-ground equivalence. In the other case, a more promising call-by-need discipline for the generation of the wanted substitutions is used. This last strategy is also adopted to show a coincidence result with open semantics.
By minor changes, all of the above characterizations for late semantics can be suited for congruences of the early family.
Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure
Authors: Danvy Olivier , Schultz Ulrik P.
Published: February 2016

Lambda-lifting a functional program transforms it into a set of recursive
equations. We present the symmetric transformation: lambda-dropping.
Lambda-dropping a set of recursive equations restores block
structure and lexical scope.
For lack of scope, recursive equations must carry around all the
parameters that any of their callees might possibly need. Both lambda-lifting
and lambda-dropping thus require one to compute a transitive
closure over the call graph:

- for lambda-lifting: to establish the Def/Use path of each free
variable (these free variables are then added as parameters to
each of the functions in the call path);

- for lambda-dropping: to establish the Def/Use path of each parameter
(parameters whose use occurs in the same scope as their
definition do not need to be passed along in the call path).
Without free variables, a program is scope-insensitive. Its blocks are
then free to float (for lambda-lifting) or to sink (for lambda-dropping)
along the vertices of the scope tree.

We believe lambda-lifting and lambda-dropping are interesting per
se, both in principle and in practice, but our prime application is partial
evaluation: except for Malmkjær and Ørbæk's case study presented at
PEPM'95, most polyvariant specializers for procedural programs operate
on recursive equations. To this end, in a pre-processing phase,
they lambda-lift source programs into recursive equations. As a result,
residual programs are also expressed as recursive equations, often with
dozens of parameters, which most compilers do not handle efficiently.
Lambda-dropping in a post-processing phase restores their block structure
and lexical scope thereby significantly reducing both the compile
time and the run time of residual programs.

 