@string{brics =	"{BRICS}"}
@string{daimi =	"Department of Computer Science, University of Aarhus"}
@string{iesd  =	"Department of Mathematics and Computer Science, Aalborg University"}
@string{rs    =	"Research Series"}
@string{ns    =	"Notes Series"}
@string{ls    =	"Lecture Series"}
@string{ds    =	"Dissertation Series"}

  author = 	 "Torben Bra{\"u}ner",
  title = 	 "An Axiomatic Approach to Adequacy",
  institution =  brics,
  year = 	 1996,
  type = 	 ds,
  number = 	 "DS-96-4",
  address = 	 daimi,
  month = 	 nov,
  note =	 "Ph.D. thesis. 168~pp",
  abstract =	 "This thesis studies adequacy for PCF-like languages in a
		  general categorical framework. An adequacy result relates
		  the denotational semantics of a program to its
		  operational semantics; it typically states that a program
		  terminates whenever the interpretation is non-bottom. The
		  main concern is to generalise to a linear version of PCF
		  the adequacy results known for standard PCF, keeping in
		  mind that there exists a Girard translation from PCF to
		  linear PCF with respect to which the new constructs
		  should be sound. General adequacy results have usually
		  been obtained in order-enriched categories, that is,
		  categories where all hom-sets are typically cpos, maps
		  are assumed to be continuous and fixpoints are
		  interpreted using least upper bounds. One of the main
		  contributions of the thesis is to propose a completely
		  different approach to the problem of axiomatising those
		  categories which yield adequate semantics for PCF and
		  linear PCF. The starting point is that the only
		  unavoidable assumption for dealing with adequacy is the
		  existence, in any object, of a particular ``undefined''
		  point denoting the non-terminating computation of the
		  corresponding type; hom-sets are pointed sets, and this
		  is the only required structure. In such a category of
		  pointed objects, there is a way of axiomatising fixpoint
		  operators: They are maps satisfying certain equational
		  axioms, and furthermore, satisfying a very natural
		  non-equational axiom called rational openness. It is
		  shown that this axiom is sufficient, and in a precise
		  sense necessary, for adequacy. The idea is developed in
		  the intuitionistic case (standard PCF) as well as in the
		  linear case (linear PCF), which is obtained by augmenting
		  a Curry-Howard interpretation of Intuitionistic Linear
		  Logic with numerals and fixpoint constants, appropriate
		  for the linear context. Using instantiations to concrete
		  models of the general adequacy results, various purely
		  syntactic properties of linear PCF are proved to hold",
  linkhtmlabs =	 "",
  linkps =	 "",
  linkpdf =	 ""

  author = 	 "Lars Arge",
  title = 	 "Efficient External-Memory Data Structures and Applications",
  institution =  brics,
  year = 	 1996,
  type = 	 ds,
  number = 	 "DS-96-3",
  address = 	 daimi,
  month = 	 aug,
  note =	 "Ph.D. thesis. xii+169~pp",
  abstract =	 "\bgroup\def\a{algorithms}
In this thesis we study the Input/Output (I/O) complexity
of large-scale problems arising e.g. in the areas of
database systems, geographic information systems, VLSI
design systems and computer graphics, and design
I/O-efficient \a{} for them.\bibpar
A general theme in our work is to design I/O-efficient
\a{} through the design of I/O-efficient data
structures. One of our philosophies is to try to design
I/O \a{} from internal memory \a{} by
exchanging the data structures used in internal memory
with their external memory counterparts. The results in
the thesis include a technique for transforming an
internal memory tree data structure into an external data
structure which can be used in a {\em batched\/} dynamic
setting, that is, a setting where we for example do not
require that the result of a search operation is returned
immediately. Using this technique we develop batched
dynamic external versions of the (one-dimensional)
range-tree and the segment-tree and we develop an
external priority queue. These structures can be used in
standard internal memory sorting \a{} and
\a{} for problems involving geometric objects. The
latter has applications to VLSI design. Using the
priority queue we improve upon known I/O \a{} for
fundamental graph problems, and develop new efficient
\a{} for the graph-related problem of ordered
binary-decision diagram manipulation. Ordered
binary-decision diagrams are the state-of-the-art data
structure for boolean function manipulation and they are
extensively used in large-scale applications like logic
circuit verification.\bibpar
Combining our batched dynamic segment tree with the novel
technique of external-memory fractional cascading we
develop I/O-efficient \a{} for a large number of
geometric problems involving line segments in the plane,
with applications to geographic informations
systems. Such systems frequently handle huge amounts of
spatial data and thus they require good use of
external-memory techniques.\bibpar
We also manage to use the ideas in the batched dynamic
segment tree to develop ``on-line'' external data
structures for a special case of two-dimensional range
searching with applications to databases and constraint
logic programming. We develop an on-line external version
of the segment tree, which improves upon the previously
best known such structure, and an optimal on-line
external version of the interval tree. The last result
settles an important open problem in databases and I/O
\a. In order to develop these structure we use a
novel balancing technique for search trees which can be
regarded as weight-balancing of B-trees.\bibpar
Finally, we develop a technique for transforming internal
memory lower bounds to lower bounds in the I/O model, and
we prove that our new ordered binary-decision diagram
manipulation \a{} are asymptotically optimal among
a class of \a{} that include all know manipulation
  linkhtmlabs =	 "",
  linkps =	 "",
  linkpdf =	 ""

  author = 	 "Allan Cheng",
  title = 	 "Reasoning About Concurrent Computational Systems",
  institution =  brics,
  year = 	 1996,
  type = 	 ds,
  number = 	 "DS-96-2",
  address = 	 daimi,
  month = 	 aug,
  note =	 "Ph.D. thesis. xiv+229~pp",
  abstract =	 "This thesis consists of three parts. The first presents
		  contributions in the field of verification of finite
		  state concurrent systems, the second presents
		  contributions in the field of behavioural reasoning about
		  concurrent systems based on the notions of behavioural
		  preorders and behavioural equivalences, and, finally, the
		  third presents contributions in the field of set
		  In the first part, we study the computational complexity
		  of several standard verification problems for 1-safe
		  Petri nets and some of its subclasses. Our results
		  provide the first systematic study of the computational
		  complexity of these problems.\bibpar
		  We then investigate the computational complexity of a
		  more general verification problem, model-checking, when
		  an instance of the problem consists of a formula and a
		  description of a system whose state space is at most
		  exponentially larger than the description.\bibpar
		  We continue by considering the problem of performing
		  model-checking relative to a partial order semantics of
		  concurrent systems, in which not all possible sequences
		  of actions are considered relevant. We provide the first,
		  to the best of our knowledge, set of sound and complete
		  tableau rules for a CTL-like logic interpreted under
		  progress fairness assumptions. \bibpar
		  In the second part, we investigate Joyal, Nielsen, and
		  Winskel's proposal of spans of open maps as an abstract
		  category-theoretic way of adjoining a bisimulation
		  equivalence, ${\cal P}$-bisimilarity, to a category of
		  models of computation ${\cal M}$. We show that a
		  representative selection of well-known bisimulations and
		  behavioural equivalences can be captured in the setting
		  of spans of open maps.\bibpar
		  We then define the notion of functors being ${\cal
		  P}$-factorisable and show how this ensures that ${\cal
		  P}$-bisimilarity is a congruence with respect to such
		  functors. \bibpar
		  In the last part we investigate set constraints. Set
		  constraints are inclusion relations between expressions
		  denoting sets of ground terms over a ranked
		  alphabet. They are typically derived from the syntax of a
		  program and solutions to them can yield useful
		  information for, e.g., type inference, implementations,
		  and optimisations.\bibpar
		  We provide a complete Gentzen-style axiomatisation for
		  sequents $\Phi\vdash\Psi$, where $\Phi$ and $\Psi$ are
		  finite sets of set constraints, based on the axioms of
		  termset algebra. We show that the deductive system is
		  complete for the restricted sequents $\Phi\vdash\bot$
		  over standard models, incomplete for general sequents
		  $\Phi\vdash\Psi$ over standard models, but complete for
		  general sequents over set-theoretic termset
		  We then continue by investigating Kozen's rational
		  spaces.  We give several interesting results, among
		  others a Myhill-Nerode like characterisation of rational
  linkhtmlabs =	 "",
  linkps =	 "",
  linkpdf =	 ""

  author = 	 "Urban Engberg",
  title = 	 "Reasoning in the Temporal Logic of Actions --- The design
		  and implementation of an interactive computer system",
  institution =  brics,
  year = 	 1996,
  type = 	 ds,
  number = 	 "DS-96-1",
  address = 	 daimi,
  month = 	 aug,
  note =	 "Ph.D. thesis. xvi+222~pp",
  abstract =	 "Reasoning about algorithms stands out as an essential
		  challenge of computer science.  Much work has been put
		  into the development of formal methods, within recent
		  years focusing especially on concurrent algorithms.  The
		  Temporal Logic of Actions (TLA) is one of the formal
		  frameworks that has been the result of such research.  In
		  TLA a system and its properties may be specified as
		  logical formulas, allowing the application of reasoning
		  without any intermediate translation.  Being a
		  linear-time temporal logic, it easily expresses liveness
		  as well as safety properties.\bibpar
		  TLP, the TLA Prover, is a system developed by the author
		  for doing mechanical reasoning in TLA.  TLP is a complex
		  system that combines different reasoning techniques to be
		  able to handle verification of real systems.  It uses the
		  Larch Prover as its main verification back-end, but as
		  well makes it possible to utilize results provided by
		  other back-ends, such as an automatic linear-time
		  temporal logic checker for finite-state systems.
		  Specifications to be verified within the TLP system are
		  written in a dedicated language, an extension of pure
		  TLA.  The language as well contains syntactical
		  constructs for representing natural deduction proofs, and
		  a separate language for defining methods to be applied
		  during verification.  With the TLP translators and
		  interactive front-end, it is possible to write
		  specifications and incrementally develop mechanically
		  verifiable proofs in a fashion that has not been seen
  linkhtmlabs =	 "",
  linkps =	 "",
  linkpdf =	 ""