@string{brics = "{BRICS}"}
@string{daimi = "Department of Computer Science, University of Aarhus"}
@string{iesd = "Department of Computer Science, Institute
of Electronic Systems, Aalborg University"}
@string{rs = "Research Series"}
@string{ns = "Notes Series"}
@string{ls = "Lecture Series"}
@string{ds = "Dissertation Series"}
@TechReport{BRICS-RS-07-18,
author = "Midtgaard, Jan",
title = "Control-Flow Analysis of Functional Programs",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-18",
address = daimi,
OPTkey = "",
month = dec,
note = "iii+38~pp",
abstract = "We present a survey of control-flow analysis of
functional programs, which has been the subject of
extensive investigation throughout the past 25
years. Analyses of the control flow of functional
programs have been formulated in multiple settings
and have led to many different approximations,
starting with the seminal works of Jones, Shivers,
and Sestoft. In this paper we survey control-flow
analysis of functional programs by structuring the
multitude of formulations and approximations and
comparing them",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-17,
author = "Aceto, Luca and Fokkink, Willem Jan and
Ing{\'o}lfsd{\'o}ttir, Anna",
title = "A Cancellation Theorem for {7BCCSP}",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-17",
address = "Reykjavik University",
OPTkey = "",
month = dec,
note = "30~pp",
abstract = "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.",
OPTlinkhtmlabs ="",
OPTlinkdvi = "",
OPTlinkps = "",
OPTlinkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-16,
author = "Danvy, Olivier and Millikin, Kevin",
title = "On the Equivalence between Small-Step and Big-Step
Abstract Machines: A Simple Application of
Lightweight Fusion",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-16",
address = daimi,
OPTkey = "",
month = nov,
note = "ii+11~pp. To appear in {\em Information Processing
Letters} (extended version). Supersedes BRICS
RS-07-8",
abstract = " 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.\bibpar 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).",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-15,
author = "Lee, Jooyong",
title = "A Case for Dynamic Reverse-code Generation",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-15",
address = daimi,
OPTkey = "",
month = aug,
note = "ii+10~pp",
abstract = "Backtracking (i.e.\ reverse execution) helps the user
of a debugger to naturally think backwards along the
execution path of a program, and thinking backwards
makes it easy to locate the origin of a bug. So far
backtracking has been implemented mostly by state
saving or by checkpointing. These implementations,
however, inherently do not scale. As has often been
said, the ultimate solution for backtracking is to
use reverse code: executing the reverse code
restores the previous states of a program. In our
earlier work, we presented a method to generate
reverse code on the fly while running a
debugger. This article presents a case study of
dynamic reverse-code generation. We compare the
memory usage of various backtracking methods in a
simple but nontrivial example, a bounded-buffer
program. In the case of non-deterministic programs
such as this bounded-buffer program, our dynamic
reverse-code generation can outperform the existing
backtracking methods in terms of memory efficiency.",
OPTlinkhtmlabs ="",
OPTlinkdvi = "",
OPTlinkps = "",
OPTlinkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-14,
author = "Danvy, Olivier and Spivey, Michael",
title = "On {B}arron and {S}trachey's Cartesian Product
Function",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-14",
address = daimi,
OPTkey = "",
month = jul,
note = "ii+14~pp",
abstract = "Over forty years ago, David Barron and Christopher
Strachey published a startlingly elegant program for
the Cartesian product of a list of lists, expressing
it with a three nested occurrences of the function
we now call \emph{foldr}. This program is remarkable
for its time because of its masterful display of
higher-order functions and lexical scope, and we put
it forward as possibly the first ever functional
pearl. We first characterize it as the result of a
sequence of program transformations, and then apply
similar transformations to a program for the
classical power set example. We also show that using
a higher-order representation of lists allows a
definition of the Cartesian product function where
\emph{foldr} is nested only twice.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-13,
author = "Lange, Martin",
title = "Temporal Logics Beyond Regularity",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-13",
address = daimi,
OPTkey = "",
month = jul,
note = "82~pp",
abstract = "Non-regular program correctness properties play an
important role in the specification of unbounded
buffers, recursive procedures, etc. This thesis
surveys results about the relative expressive power
and complexity of temporal logics which are capable
of defining non-regular properties. In particular,
it features Propositional Dynamic Logic of
Context-Free Programs, Fixpoint Logic with Chop, the
Modal Iteration Calculus, and Higher-Order Fixpoint
Logic.\bibpar Regarding expressive power we consider
two classes of structures: arbitrary transition
systems as well as finite words as a subclass of the
former. The latter is meant to give an intuitive
account of the logics' expressive powers by relating
them to known language classes defined in terms of
grammars or Turing Machines. \bibpar Regarding the
computational complexity of temporal logics beyond
regularity we focus on their model checking problems
since their satisfiability problems are all highly
undecidable. Their model checking complexities range
between polynomial time and non-elementary. ",
OPTlinkhtmlabs ="",
OPTlinkdvi = "",
OPTlinkps = "",
OPTlinkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-12,
author = "Brodal, Gerth St{\o}lting and Fagerberg, Rolf and
J{\o}rgensen, Allan Gr{\o}nlund and Moruz, Gabriel and
M{\o}lhave, Thomas",
title = "Optimal Resilient Dynamic Dictionaries",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-12",
address = daimi,
OPTkey = "",
month = jul,
OPTnote = "~pp",
OPTabstract = "",
OPTlinkhtmlabs ="",
OPTlinkdvi = "",
OPTlinkps = "",
OPTlinkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-11,
author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
title = "The Saga of the Axiomatization of Parallel
Composition",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-11",
address = iesd,
OPTkey = "",
month = jun,
note = "15~pp. To appear in the Proceedings of CONCUR 2007,
the 18th International Conference on Concurrency
Theory (Lisbon, Portugal, September 4--7, 2007),
Lecture Notes in Computer Science, Springer-Verlag,
2007",
abstract = "This paper surveys some classic and recent results
on the finite axiomatizability of bisimilarity over
CCS-like languages. It focuses, in particular, on
non-finite axiomatizability results stemming from
the semantic interplay between parallel composition
and nondeterministic choice. The paper also
highlights the role that auxiliary operators, such
as Bergstra and Klop's left and communication merge
and Hennessy's merge operator, play in the search
for a finite, equational axiomatization of parallel
composition both for classic process algebras and
for their real-time extensions",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-10,
author = "Brabrand, Claus and Giegerich, Robert and M{\o}ller,
Anders",
title = "Analyzing Ambiguity of Context-Free Grammars",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-10",
address = daimi,
OPTkey = "",
month = may,
note = "17~pp. Full version of paper presented at CIAA~'07",
abstract = "It has been known since 1962 that the ambiguity
problem for context-free grammars is
undecidable. Ambiguity in context-free grammars is a
recurring problem in language design and parser
generation, as well as in applications where
grammars are used as models of real-world physical
structures.\bibpar We observe that there is a simple
linguistic characterization of the grammar ambiguity
problem, and we show how to exploit this to
conservatively approximate the problem based on
local regular approximations and grammar
unfoldings. As an application, we consider grammars
that occur in RNA analysis in bioinformatics, and we
demonstrate that our static analysis of context-free
grammars is sufficiently precise and efficient to be
practically useful",
linkhtmlabs = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-9,
author = "Nielsen, Janus Dam and Schwartzbach, Michael I.",
title = "The {SMCL} Language Specification",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-9",
address = daimi,
OPTkey = "",
month = mar,
OPTnote = "~pp",
OPTabstract = "",
OPTlinkhtmlabs ="",
OPTlinkdvi = "",
OPTlinkps = "",
OPTlinkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-8,
author = "Danvy, Olivier and Millikin, Kevin",
title = "A Simple Application of Lightweight Fusion to
Proving the Equivalence of Abstract Machines",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-8",
address = daimi,
OPTkey = "",
month = mar,
note = "ii+6~pp",
abstract = "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",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-7,
author = "Danvy, Olivier and Millikin, Kevin",
title = "Refunctionalization at Work",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-7",
address = daimi,
OPTkey = "",
month = mar,
note = "ii+16~pp. Invited talk at the 8th International
Conference on Mathematics of Program Construction,
MPC '06",
abstract = "We present the left inverse of Reynolds's
defunctionalization and we show its relevance to
programming and to programming languages. We present
two methods to put a program that is almost in
defunctionalized form into one that is actually in
defunctionalized form, and we illustrate them with a
recognizer for Dyck words and with Dijkstra's
shunting-yard algorithm",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-6,
author = "Danvy, Olivier and Millikin, Kevin and Nielsen,
Lasse R.",
title = "On One-Pass {CPS} Transformations",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-6",
address = daimi,
OPTkey = "",
month = mar,
note = "ii+19~pp. Theoretical Pearl appeara in the {\em
Journal of Functional Programming}, 17(6), p.\
793--812, January 2007. Revised version of BRICS
RS-02-3",
abstract = "We bridge two distinct approaches to one-pass CPS
transformations, i.e., CPS transformations that
reduce administrative redexes at transformation time
instead of in a post-processing phase. One approach
is compositional and higher-order, and is
independently due to Appel, Danvy and Filinski, and
Wand, building on Plotkin's seminal work. The other
is non-compositional and based on a reduction
semantics for the lambda-calculus, and is due to
Sabry and Felleisen. To relate the two approaches,
we use three tools: Reynolds's defunctionalization
and its left inverse, refunctionalization; a special
case of fold-unfold fusion due to Ohori and Sasano,
fixed-point promotion; and an implementation
technique for reduction semantics due to Danvy and
Nielsen, refocusing.\bibpar This work is directly
applicable to transforming programs into monadic
normal form.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-5,
author = "Aceto, Luca and Capobianco, Silvio and
Ing{\'o}lfsd{\'o}ttir, Anna",
title = "On the Existence of a Finite Base for Complete Trace
Equivalence over {BPA} with Interrupt",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-5",
address = iesd,
OPTkey = "",
month = feb,
note = "26~pp",
abstract = "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",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-4,
author = "St{\o}vring, Kristian and Lassen, S{\o}ren B.",
title = "A Complete, Co-Inductive Syntactic Theory of
Sequential Control and State",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-4",
address = daimi,
OPTkey = "",
month = feb,
note = "36~pp. Appears in the proceedings of POPL 2007,
p. 161--172",
abstract = "We present a new co-inductive syntactic theory,
eager normal form bisimilarity, for the untyped
call-by-value lambda calculus extended with
continuations and mutable references.\bibpar We
demonstrate that the associated bisimulation proof
principle is easy to use and that it is a powerful
tool for proving equivalences between recursive
imperative higher-order programs.\bibpar The theory
is modular in the sense that eager normal form
bisimilarity for each of the calculi extended with
continuations and/or mutable references is a fully
abstract extension of eager normal form bisimilarity
for its sub-calculi. For each calculus, we prove
that eager normal form bisimilarity is a congruence
and is sound with respect to contextual
equivalence. Furthermore, for the calculus with both
continuations and mutable references, we show that
eager normal form bisimilarity is complete: it
coincides with contextual equivalence.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-3,
author = "Aceto, Luca and Fokkink, Willem Jan and
Ing{\'o}lfsd{\'o}ttir, Anna",
title = "Ready To Preorder: Get Your {BCCSP} Axiomatization for
Free!",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-3",
address = iesd,
OPTkey = "",
month = feb,
note = "37~pp",
abstract = "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",
linkhtmlabs = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-2,
author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
title = "Characteristic Formulae: From Automata to Logic",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-2",
address = iesd,
OPTkey = "",
month = jan,
note = "18~pp",
abstract = "This paper discusses the classic notion of
characteristic formulae for processes using
variations on Hennessy-Milner logic as the
underlying logical specification language. It is
shown how to characterize logically (states of)
finite labelled transition systems modulo
bisimilarity using a single formula in
Hennessy-Milner logic with recursion. Moreover,
characteristic formulae for timed automata with
respect to timed bisimilarity and the faster-than
preorder of Moller and Tofts are offered in terms of
the logic $L_{\nu}$ of Laroussinie, Larsen and
Weise.",
linkhtmlabs = "",
linkdvi = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}
@TechReport{BRICS-RS-07-1,
author = "Andersson, Daniel",
title = "{HIROIMONO} is {NP}-complete",
institution = brics,
year = 2007,
type = rs,
number = "RS-07-1",
address = daimi,
OPTkey = "",
month = jan,
note = "8~pp",
abstract = "In a Hiroimono puzzle, one must collect a set of
stones from a square grid, moving along grid lines,
picking up stones as one encounters them, and
changing direction only when one picks up a
stone. We show that deciding the solvability of such
puzzles is NP-complete",
linkhtmlabs = "",
linkps = "",
linkpdf = "",
OPTannote = ""
}