@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-94-48,
author = "Godskesen, Jens Chr{.} and Larsen, Kim G.",
title = "Synthesizing Distinguishing Formulae for Real
Time Systems",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-48",
address = iesd,
month = dec,
note = "21~pp. Extended abstract appears in " #
lncs969 # ", pages 519--528",
abstract = "This paper describes a technique for
generating diagnostic information for the {\sl
timed} bisimulation equivalence and the {\sl
timed} simulation preorder. More precisely,
given two (parallel) networks of regular
real--time processes, the technique will
provide a logical formula that differentiates
them in case they are not timed (bi)similar.
Our method may be seen as an extension of the
algorithm by {\v C}er{\=a}ns for deciding timed
bisimilarity in that information of
time--quantities has been added sufficient for
generating distinguishing formulae. The
technique has been added to the automatic
verification tool {\sc Epsilon} and applied to
various examples.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-47,
author = "Larsen, Kim G. and Steffen, Bernhard and
Weise, Carsten",
title = "A Constraint Oriented Proof Methodology based
on Modal Transition Systems",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-47",
address = iesd,
month = dec,
note = "13 pp",
abstract = "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
{\em projective views}, {\em separation of
proof obligations}, {\em Skolemization} and
{\em abstraction}. The method is even
applicable to real time systems.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-46,
author = "Beimel, Amos and G{\'a}l, Anna and Paterson,
Mike",
title = "Lower Bounds for Monotone Span Programs",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-46",
address = daimi,
month = dec,
note = "14~pp. Appears in " # ieeefocs95 # ", pages
674--681",
abstract = "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.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-45,
author = "Andersen, J{\o}rgen H. and Kristoffersen,
K{\aa}re J. and Larsen, Kim G. and Niedermann,
Jesper",
title = "Automatic Synthesis of Real Time Systems",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-45",
address = iesd,
month = dec,
note = "17 pp. Appears in " # lncs944 # ", pages
535--546",
abstract = "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\,{\mid
}\,\ldots\,{\mid}\,A_n\,{\mid}\,X) \,\,\mbox
{{\sf sat}}\,\, S \] where $S$ is a real time
(logical) specification, $A_1\ldots 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\ldots 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.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-94-44,
author = "Agerholm, Sten",
title = "A {HOL} Basis for Reasoning about Functional
Programs",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-44",
address = daimi,
month = dec,
note = "PhD thesis. viii+224 pp",
abstract = "Domain theory is the mathematical theory
underlying denotational semantics. This thesis
presents a formalization of domain theory in
the Higher Order Logic (HOL) theorem proving
system along with a mechanization of proof
functions and other tools to support reasoning
about the denotations of functional programs.
By providing a fixed point operator for
functions on certain domains which have a
special undefined (bottom) element, this
extension of HOL supports the definition of
recursive functions which are not also
primitive recursive. Thus, it provides an
approach to the long-standing and important
problem of defining non-primitive recursive
functions in the HOL system.\bibpar
Our philosophy is that there must be a direct
correspondence between elements of complete
partial orders (domains) and elements of HOL
types, in order to allow the reuse of higher
order logic and proof infrastructure already
available in the HOL system. Hence, we are able
to mix domain theoretic reasoning with
reasoning in the set theoretic HOL world to
advantage, exploiting HOL types and tools
directly. Moreover, by mixing domain and set
theoretic reasoning, we are able to eliminate
almost all reasoning about the bottom element
of complete partial orders that makes the LCF
theorem prover, which supports a first order
logic of domain theory, difficult and tedious
to use. A thorough comparison with LCF is
provided.\bibpar
The advantages of combining the best of the
domain and set theoretic worlds in the same
system are demonstrated in a larger example,
showing the correctness of a unification
algorithm. A major part of the proof is
conducted in the set theoretic setting of
higher order logic, and only at a late stage of
the proof domain theory is introduced to give a
recursive definition of the algorithm, which is
not primitive recursive. Furthermore, a total
well-founded recursive unification function can
be defined easily in pure HOL by proving that
the unification algorithm (defined in domain
theory) always terminates; this proof is
conducted by a non-trivial well-founded
induction. In such applications, where
non-primitive recursive HOL functions are
defined via domain theory and a proof of
termination, domain theory constructs only
appear temporarily.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-94-43,
author = "Aceto, Luca and Jeffrey, Alan~S.~A.",
title = "A Complete Axiomatization of Timed
Bisimulation for a Class of Timed Regular
Behaviours (Revised Version)",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-43",
address = iesd,
month = dec,
note = "18 pp. Appears in {\em Theoretical Computer
Science} vol.~152(2) pages 251--268, December
1995",
abstract = "One of the most satisfactory results in
process theory is Milner's axiomatization of
strong bisimulation for regular CCS. This
result holds for open terms with finite-state
recursion. Wang has shown that timed
bisimulation can also be axiomatized, but only
for closed terms without recursion. In this
paper, we provide an axiomatization for timed
bisimulation of open terms with finite-state
recursion.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-42,
author = "Breslauer, Dany and G{\c{a}}sieniec, Leszek",
title = "Efficient String Matching on Coded Texts",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-42",
address = daimi,
month = dec,
note = "20 pp. Appears with the title {\em Efficient
String Matching on Packed Texts} in " # lncs937
# ", pages 27--40 and in {\em RAIRO
Informatique Th{\'e}orique et Applications},
30(6):521--544, 1996",
abstract = "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.\bibpar
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.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-41,
author = "Miltersen, Peter Bro and Nisan, Noam and
Safra, Shmuel and Wigderson, Avi",
title = "On Data Structures and Asymmetric
Communication Complexity",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-41",
address = daimi,
month = dec,
note = "17 pp. Appears in " # acmstoc95 # ", pages
103--111. Appears also in {\em Journal of
Computer and System Sciences}, 57(1):37--49,
1998",
abstract = "In this paper we consider two party
communication complexity when the input sizes
of the two players differ significantly, the
``asymmetric'' case. Most of previous work on
communication complexity only considers the
total number of bits sent, but we study
tradeoffs between the number of bits the first
player sends and the number of bits the second
sends. These types of questions are closely
related to the complexity of static data
structure problems in the cell probe model. We
derive two generally applicable methods of
proving lower bounds, and obtain several
applications. These applications include new
lower bounds for data structures in the cell
probe model. Of particular interest is our
``round elimination'' lemma, which is
interesting also for the usual symmetric
communication case. This lemma generalizes and
abstracts in a very clean form the ``round
reduction'' techniques used in many previous
lower bound proofs.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-40,
author = "Aceto, Luca and Ing{\'o}lfsd{\'o}ttir, Anna",
title = "{CPO} Models for {GSOS} Languages --- Part
{I}: Compact {GSOS} Languages",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-40",
address = iesd,
month = dec,
note = "70 pp. An extended abstract of the paper
appears in: {\em Proceedings of CAAP~'95}, LNCS
915, 1995, pages 439--453. Full version also
appears in {\em Information and Computation},
129(2):107--141, September 1996.",
abstract = "In this paper, we present a general way of
giving denotational semantics to a class of
languages equipped with an operational
semantics that fits the GSOS format of Bloom,
Istrail and Meyer. The canonical model used for
this purpose will be Abramsky's domain of
synchronization trees, and the denotational
semantics automatically generated by our
methods will be guaranteed to be fully abstract
with respect to the finitely observable part of
the bisimulation preorder. In the process of
establishing the full abstraction result, we
also obtain several general results on the
bisimulation preorder (including a complete
axiomatization for it), and give a novel
operational interpretation of GSOS languages",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-39,
author = "Damg{\aa}rd, Ivan B. and Goldreich, Oded and
Wigderson, Avi",
title = "Hashing Functions can Simplify Zero-Knowledge
Protocol Design (too)",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-39",
address = daimi,
month = nov,
note = "18 pp",
abstract = "In {\em Crypto93}, Damg{\aa}rd showed that
any constant-round protocol in which the
verifier sends only independent, random bits
and which is zero-knowledge against the {\em
honest} verifier can be transformed into a
protocol (for the same problem) that is
zero-knowledge {\em in general}. His
transformation was based on the interactive
hashing technique of Naor, Ostrovsky,
Venkatesan and Yung, and thus the resulting
protocol had very large
round-complexity.\bibpar
We adopt Damg{\aa}rd's methods, using ordinary
hashing functions, instead of the
abovementioned interactive hashing technique.
Typically, the protocols we derive have much
lower round-complexity than those derived by
Damg{\aa}rd's transformation. As in
Damg{\aa}rd's transformation, our
transformation preserves statistical/perfect
zero-knowledge and does not rely on any
computational assumptions. However, unlike
Damg{\aa}rd's transformation, the new
transformation is not applicable to argument
systems or to proofs of knowledge",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-38,
author = "Damg{\aa}rd, Ivan B. and Knudsen, Lars
Ramkilde",
title = "Enhancing the Strength of Conventional
Cryptosystems",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-38",
address = daimi,
month = nov,
note = "12 pp",
abstract = "We look at various ways of enhancing the
strength of conventional cryptosystems such as
DES by building a new system which has longer
keys and which uses the original system as a
building block. We propose a new variant of
two-key triple encryption which is not
vulnerable to the meet in the middle attack by
van Oorschot and Wiener. Under an appropriate
assumption on the security of DES, we can prove
that our system is at least as hard to break as
single DES",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-37,
author = "van Oosten, Jaap",
title = "Fibrations and Calculi of Fractions",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-37",
address = daimi,
month = nov,
note = "21 pp. Appears in {\em Journal of Pure and
Applied}, 146(1):77--102, 2000",
abstract = "Given a fibration ${\cal E}\rightarrow\cal B$
and a class $\Sigma$ of arrows of $\cal B$, one
can construct the free fibration (on $\cal E$
over $\cal B$ such that all reindexing functors
over elements of $\Sigma$ are
equivalences.\bibpar
In this work I give an explicit construction of
this, and study its properties. For example,
the construction preserves the property of
being fibrewise discrete, and it commutes up to
equivalence with fibrewise exact completions. I
show that mathematically interesting situations
are examples of this construction. In
particular, subtoposes of the effective topos
are treated.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-36,
author = "Razborov, Alexander A.",
title = "On provably disjoint {{\bf NP}}-pairs",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-36",
address = daimi,
month = nov,
note = "27 pp",
abstract = "In this paper we study the pairs $(U,V)$ of
disjoint {\bf NP}-sets representable in a
theory $T$ of Bounded Arithmetic in the sense
that $T$ proves $U \cap V = \emptyset$. For a
large variety of theories $T$ we exhibit a
natural disjoint {\bf NP}-pair which is
complete for the class of disjoint {\bf
NP}-pairs representable in $T$. This allows us
to clarify the approach to showing independence
of central open questions in Boolean complexity
from theories of Bounded Arithmetic initiated
in [1]. Namely, in order to prove the
independence result from a theory $T$, it is
sufficient to separate the corresponding
complete {\bf NP}-pair by a (quasi)poly-time
computable set. We remark that such a
separation is obvious for the theory ${\cal
S}(S_2) + {\cal S}\Sigma^b_2 - PIND$ considered
in [1], and this gives an alternative proof of
the main result from that paper.\bibpar
[1] A. Razborov. Unprovability of lower bounds
on circuit size in certain fragments of Bounded
Arithmetic. To appear in {\em Izvestiya of the
RAN}, 1994. ",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-35,
author = "Brodal, Gerth St{\o}lting",
title = "Partially Persistent Data Structures of
Bounded Degree with Constant Update Time",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-35",
address = daimi,
month = nov,
note = "24~pp. Appears in {\em Nordic Journal of
Computing}, 3(3):238--255, 1996",
abstract = "The problem of making bounded in-degree and
out-degree data structures partially persistent
is considered. The node copying method of
Driscoll {\it et al.\/} is extended so that
updates can be performed in {\em worst-case\/}
constant time on the pointer machine model.
Previously it was only known to be possible in
amortised constant time [Driscoll89].
The result is presented in terms of a new
strategy for Dietz and Raman's dynamic two
player pebble game on graphs.
It is shown how to implement the strategy and
the upper bound on the required number of
pebbles is improved from $2b+2d+O(\sqrt{b})$ to
$d+2b$, where $b$ is the bound of the in-degree
and $d$ the bound of the out-degree. We also
give a lower bound that shows that the number
of pebbles depends on the out-degree $d$.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-94-34,
author = "Andersen, Henrik Reif and Stirling, Colin and
Winskel, Glynn",
title = "A Compositional Proof System for the Modal
$\mu$-Calculus",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-34",
address = daimi,
month = oct,
note = "18~pp. Appears in " # lics9 # ", pages
144--153. Superseeded by BRICS Report
RS-98-40",
abstract = "We present a proof system for determining
satisfaction between processes in a fairly
general process algebra and assertions of the
modal $\mu$-calculus. The proof system is
compositional in the structure of processes. It
extends earlier work on compositional reasoning
within the modal $\mu$-calculus and combines it
with techniques from work on local model
checking. The proof system is sound for all
processes and complete for a class of
finite-state processes.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-33,
author = "Sassone, Vladimiro",
title = "Strong Concatenable Processes: An Approach to
the Category of Petri Net Computations",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-33",
address = daimi,
month = oct,
note = "40 pp. Workshop version appears in " # nwpt6 #
", pages 385--399 with the title {\em An
Approach to the Category of Net Computations}.
Revised version appears in " # lncs915 # ",
pages 334--348 with the title {\em On the
Category of {P}etri Net Computations}",
abstract = "We introduce the notion of {\it strong
concatenable process\/} for Petri nets as the
least refinement of non-sequential
(concatenable) processes which can be expressed
abstractly by means of a {\it functor\/} ${\cal
Q}[\_]$ from the category of Petri nets to an
appropriate category of symmetric strict
monoidal categories with free non-commutative
monoids of objects, in the precise sense that,
for each net~$N$, the strong concatenable
processes of~$N$ are isomorphic to the arrows
of~${\cal Q}[N]$. This yields an axiomatization
of the causal behaviour of Petri nets in terms
of symmetric strict monoidal categories.\bibpar
In addition, we identify a {\it coreflection\/}
right adjoint to ${\cal Q}[\_]$ and we
characterize its replete image in the category
of symmetric monoidal categories, thus yielding
an abstract description of the category of net
computations",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-32,
author = "Aiken, Alexander and Kozen, Dexter and
Wimmers, Ed",
title = "Decidability of Systems of Set Constraints
with Negative Constraints",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-32",
address = daimi,
month = oct,
note = "33 pp. Appears in {\em Information and Computation},
122(1):30-44, October 1995",
abstract = "Set constraints are relations between sets of
terms. They have been used extensively in
various applications in program analysis and
type inference. Recently, several algorithms
for solving general systems of positive set
constraints have appeared. In this paper we
consider systems of mixed positive and negative
constraints, which are considerably more
expressive than positive constraints alone. We
show that it is decidable whether a given such
system has a solution. The proof involves a
reduction to a number-theoretic decision
problem that may be of independent interest.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-31,
author = "Nisan, Noam and Ta-Shma, Amnon",
title = "Symmetric Logspace is Closed Under
Complement",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-31",
address = daimi,
month = sep,
note = "8 pp",
abstract = "We present a Logspace, many-one reduction
from the undirected st-connectivity problem to
its complement. This shows that $SL = co -
SL$",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-30,
author = "Husfeldt, Thore",
title = "Fully Dynamic Transitive Closure in Plane Dags
with one Source and one Sink",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-30",
address = daimi,
month = sep,
note = "26 pp. Appears in " # lncs979 # ", pages
199--212",
abstract = "We give an algorithm for the Dynamic
Transitive Closure Problem for planar directed
acyclic graphs with one source and one sink.
The graph can be updated in logarithmic time
under arbitrary edge insertions and deletions
that preserve the embedding. Queries of the
form `is there a directed path from $u$ to
$v$?' for arbitrary vertices $u$ and $v$ can be
answered in logarithmic time. The size of the
data structure and the initialisation time are
linear in the number of edges.\bibpar
The result enlarges the class of graphs for
which a logarithmic (or even polylogarithmic)
time dynamic transitive closure algorithm
exists. Previously, the only algorithms within
the stated resource bounds put restrictions on
the topology of the graph or on the delete
operation. To obtain our result, we use a new
characterisation of the transitive closure in
plane graphs with one source and one sink and
introduce new techniques to exploit this
characterisation.\bibpar
We also give a lower bound of $\Omega(\log
n/\log\log n)$ on the amortised complexity of
the problem in the cell probe model with
logarithmic word size. This is the first
dynamic directed graph problem with almost
matching lower and upper bounds.",
linkhtmlabs = "",
linkps = ""
}
@techreport{BRICS-RS-94-29,
author = "Cramer, Ronald and Damg{\aa}rd, Ivan B.",
title = "Secure Signature Schemes Based on Interactive
Protocols",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-29",
address = daimi,
month = sep,
note = "24~pp. Appears in " # lncs963 # ", pages
297--310",
abstract = "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.\bibpar
More precisely, given only an interactive
protocol of a certain type as a primitive, we
can build a (non-interactive) signature scheme
that is secure in the strongest sense of
Goldwasser, Micali and Rivest (GMR): not
existentially forgeable under adaptively chosen
message attacks. There are numerous examples of
primitives that satisfy our conditions, e.g.
Feige-Fiat-Shamir, Schnorr, Guillou-Quisquater,
Okamoto and Brickell-Mc.Curley.\bibpar
In fact, the existence of one-way group
homomorphisms is a sufficient assumption to
support our construction. As we also
demonstrate that our construction can be based
on claw-free pairs of trapdoor one-way
permutations, our results can be viewed as a
generalization of the GMR signature scheme",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-28,
author = "Goldreich, Oded",
title = "Probabilistic Proof Systems",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-28",
address = "Department of Applied Mathematics and Computer
Science, Weizmann Institute of Science,
Rehovot, Israel",
month = sep,
note = "19 pp",
abstract = "Various types of {\em probabilistic} proof
systems have played a central role in the
development of computer science in the last
decade. In this exposition, we concentrate on
three such proof systems --- {\em interactive
proofs}, {\em zero-knowledge proofs}, and {\em
probabilistic checkable proofs} --- stressing
the essential role of randomness in each of
them.\bibpar
This exposition is an expanded version of a
survey written for the proceedings of the
International Congress of Mathematicians ({\em
ICM94}) held in Zurich in 1994. It is hope that
this exposition may be accessible to a broad
audience of computer scientists and
mathematians.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-27,
author = "Bra{\"u}ner, Torben",
title = "A Model of Intuitionistic Affine Logic from
Stable Domain Theory (Revised and Expanded
Version)",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-27",
address = daimi,
month = sep,
note = "19 pp. Full version of paper appearing in " #
lncs820 # ", pages 340--351. This report is a
revised and expanded version of DAIMI IR-118",
abstract = "Girard worked with the category of coherence
spaces and continuous stable maps and observed
that the functor that forgets the linearity of
linear stable maps has a left adjoint. This
fundamental observation gave rise to the
discovery of Linear Logic. Since then, the
category of coherence spaces and linear stable
maps, with the comonad induced by the
adjunction, has been considered a canonical
model of Linear Logic. Now, the same phenomenon
is present if we consider the category of pre
dI domains and continuous stable maps, and the
category of dI domains and linear stable maps;
the functor that forgets the linearity has a
left adjoint. This gives an alternative model
of Intuitionistic Linear Logic. It turns out
that this adjunction can be factored in two
adjunctions yielding a model of Intuitionistic
Affine Logic; the category of pre dI domains
and affine stable functions. It is the goal of
this paper to show that this category is
actually a model of Intuitionistic Affine
Logic, and to show that this category moreover
has properties which make it possible to use it
to model convergence/divergence behaviour and
recursion.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-26,
author = "Riis, S{\o}ren",
title = "Count($q$) versus the Pigeon-Hole Principle",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-26",
address = daimi,
month = aug,
note = "3 pp. Appears in {\em Archive for Mathematical
Logic\/} 36(3):157--188 (1997) (expanded to a
selfcontained paper)",
abstract = "For each $p \leq 2$ there exist a model
${M\!\!I}^{*}$ of $I\Delta_{0}(\alpha)$ which
satisfies the Count($p$) principle. Furthermore
if $p$ contain all prime factors of $q$ there
exist $n,r \in{M\!\!I}^{*}$ and a bijective map
$f \in{\rm Set}({M\!\!I}^{*})$ mapping
$\{1,2,...,n\}$ onto $\{1,2,...,n+q^{r}\}$.
\bibpar
A corollary is a complete classification of the
Count($q$) versus Count($p$) problem. Another
corollary solves an open question by M.
Ajtai.",
linkhtmlabs = "",
linkdvi = "",
linkps = ""
}
@techreport{BRICS-RS-94-25,
author = "Riis, S{\o}ren",
title = "Bootstrapping the Primitive Recursive
Functions by 47 Colors",
institution = brics,
year = 1994,
type = rs,
number = "RS-94-25",
address = daimi,
month = aug,
note = "5 pp. Improved version appears in {\em Decrete
Mathematics} 169(1--3):269--272 (1997) under
the title {\em Bootstrapping the Primitive
Recursive Functions by Only 27 Colors}",
abstract = "I construct a concrete coloring of the 3
element subsets of $I\!N$. It has the property
that each homogeneous set
$\{s_{1},s_{2},...,s_{u}\}, u \geq s_{1}$ has
its elements spread so much apart that
$F_{\omega}(s_{i})